IRIS Uni Torinohttps://iris.unito.itIl sistema di repository digitale IRIS acquisisce, archivia, indicizza, conserva e rende accessibili prodotti digitali della ricerca.Mon, 09 Dec 2019 20:49:53 GMT2019-12-09T20:49:53Z10421A Polymorphic Language which is Typable and Poly-stephttp://hdl.handle.net/2318/23068Titolo: A Polymorphic Language which is Typable and Poly-step
Abstract: A functional language LambdaLAL is given. A sub-set LambdaLAL typ of LambdaLAL is automatically typable. The types are formulas of Intuitionistic Light Affine Logic with polymorphism a la ML. Every term of LambdaLALtyp can reduce to its normal form in, at most, poly-steps. LambdaLALtyp can be used as a prototype of programming language for P-TIME algorithms.
Thu, 01 Jan 1998 00:00:00 GMThttp://hdl.handle.net/2318/230681998-01-01T00:00:00ZThe call by value Lambda-calculus: a semantic investigationhttp://hdl.handle.net/2318/23064Titolo: The call by value Lambda-calculus: a semantic investigation
Abstract: This paper is about a categorical approach for modeling the pure (i.e., without constants) call-by-value lambda-calculus, defined by Plotkin as a restriction of the call-by-name lambda-calculus. In particular, the properties a category CC must enjoy to describe a model of call-by-value lambda-calculus are given. The category CC is general enough to catch models in Scott Domains and Coherence Spaces.
Fri, 01 Jan 1999 00:00:00 GMThttp://hdl.handle.net/2318/230641999-01-01T00:00:00ZMR2588403 (2011b:03087) Baillot, Patrick; Mazza, Damiano Linear logic by levels and bounded time complexity. Theoret. Comput. Sci. 411 (2010), no. 2, 470–503. (Reviewer: Luca Roversi), 03F52 (03D15)http://hdl.handle.net/2318/147813Titolo: MR2588403 (2011b:03087) Baillot, Patrick; Mazza, Damiano Linear logic by levels and bounded time complexity. Theoret. Comput. Sci. 411 (2010), no. 2, 470–503. (Reviewer: Luca Roversi), 03F52 (03D15)
Sat, 01 Jan 2011 00:00:00 GMThttp://hdl.handle.net/2318/1478132011-01-01T00:00:00ZLinear Lambda Calculus and Deep Inferencehttp://hdl.handle.net/2318/92530Titolo: Linear Lambda Calculus and Deep Inference
Abstract: We introduce a deep inference logical system SBVr which extends
SBV with Rename, a self-dual atom-renaming operator. We prove that the cut free subsystem BVr of SBVr exists. We embed the terms of linear lambda-calculus with explicit substitutions into formulas of SBVr. Our embedding recalls the one of full lambda-calculus into pi-calculus. The proof-search inside SBVr and BVr is
complete with respect to the evaluation of linear lambda-calculus with explicit substitutions. Instead, only soundness of proof search in SBVr holds. Rename is crucial to let proof-search simulate the substitution of a linear lambda-term for a variable in the course of linear beta-reduction. Despite SBVr is a minimal extension of SBV its proof-search can compute all boolean functions, exactly like linear lambda-calculus with explicit substitutions can do.
Sat, 01 Jan 2011 00:00:00 GMThttp://hdl.handle.net/2318/925302011-01-01T00:00:00ZTaming Modal Impredicativity: Superlazy Reductionhttp://hdl.handle.net/2318/84359Titolo: Taming Modal Impredicativity: Superlazy Reduction
Abstract: Pure, or type-free, Linear Logic proof nets are Turing complete once cut-elimination is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing cut- elimination to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, the conclusion of a residual of a box b interacts with a node that belongs to the proof net inside another residual of b. Technically speaking, superlazy reduction is a new notion of reduction that allows to control modal impredicativity. More speciﬁcally, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a proof net ﬁnite and predictable. Speciﬁcally, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a pure proof net via superlazy reduction.
Thu, 01 Jan 2009 00:00:00 GMThttp://hdl.handle.net/2318/843592009-01-01T00:00:00ZA local criterion for polynomial-time stratified computationshttp://hdl.handle.net/2318/85119Titolo: A local criterion for polynomial-time stratified computations
Abstract: This work is a consequence of studying the (un)relatedness of the principles that allow to implicitly characterize the polynomial time functions (PTIME) under two perspectives. One perspective is predicative recursion, where we take Safe Recursion on Notation as representative. The other perspective is structural proof theory, whose representative can be Light Aﬃne Logic (LAL). A way to make the two perspectives closer is to devise polynomial sound generalizations of LAL whose set of interesting proofs-as-programs is larger than the set LAL itself supplies. Such generalizations can be found in MS.
MS is a Multimodal Stratiﬁed framework that contains subsystems among which we can ﬁnd, at least, LAL. Every subsystem is essentially determined by two sets. The ﬁrst one is countable and ﬁnite, and supplies the modalities to form modal formulæ. The second set contains building rules to generate proof nets. We call MS multimodal because the set of modalities we can use in the types for the proof nets of a subsystem is arbitrary. MS is also stratiﬁed. This means that every box, associated to some modality, in a proof net of a subsystem can never be opened. So, inside MS, we preserve stratiﬁcation which, we recall, is the main structural proof theoretic principle that makes LAL a polynomial time sound deductive system. MS is expressive enough to contain LAL and Elementary Aﬃne Logic (EAL), which is PTIME-unsound. We supply a set of syntactic constraints on the rules that identiﬁes the PTIME-maximal subsystems of MS, i.e. the PTIME-sound subsystems that contain the largest possible number of rules. It follows a syntactic condition that discriminates among PTIME-sound and PTIME-unsound subsystems of MS: a subsystem is PTIME-sound if its rules are among the rules of some PTIME-maximal subsystem. All our proofs often use Context Semantics techniques, and in particular the geometrical conﬁguration that we call dangerous spindle: a subsystem is polytime if and only if its rules cannot build dangerous spindles.
Fri, 01 Jan 2010 00:00:00 GMThttp://hdl.handle.net/2318/851192010-01-01T00:00:00ZLive! I-Learn @ Home, versione 2007http://hdl.handle.net/2318/85657Titolo: Live! I-Learn @ Home, versione 2007
Abstract: Il CD-ROM Live! I-learn @ home è un'idea di Matteo Baldoni e Luca Roversi, realizzato da Claudio Grandi con la partecipazione di Cristina Baroglio.
Attualmente la realizzazione del CD-ROM è affidata ai Servizi ICT del Dipartimento di Informatica.
La realizzazione è stata resa possibile grazie al patrocinio del Corso di Studi in Informatica e del Dipartimento di Informatica dell'Università degli Studi di Torino.
Sul CD-ROM è disponibile la piattaforma Moodle, un supporto per l'organizzazione delle attività didattiche. Scopo del CD-ROM è il suo utilizzo off-line (ovunque ci si trovi a poter usare un PC non troppo obsoleto). Con esso, infatti, è possibile progettare/sviluppare/consultare off-line dei corsi, per poi, a breve, sincronizzare con la piattaforma I-Learn o I-Teach del corso di laurea il risultato del lavoro svolto localmente.
Il CD-ROM Live! si basa su Knoppix, versione 3.4. È un sistema operativo GNU/Linux con interfaccia grafica semplice ed intuitiva che, come anticipato, non richiede installazione: si inserisce il CD-ROM, si riavvia il PC, il sistema parte e si esplorano le offerte funzionali. Quando si ha finito il lavoro, al reboot, è possibile espellere il CD-ROM e il PC funziona esattamente come prima!
Mon, 01 Jan 2007 00:00:00 GMThttp://hdl.handle.net/2318/856572007-01-01T00:00:00ZA modular database architecture enabled to comparative sequence analysishttp://hdl.handle.net/2318/91448Titolo: A modular database architecture enabled to comparative sequence analysis
Abstract: The beginning of post-genomic era is characterized by a rising numbers of public collected genomes. The evolutionary relationship among these genomes may be caught by means of the comparative analysis of sequences, in order to identify both homologous and non-coding functional elements. In this paper we report on the on-going BIOBITS project. It is focused on studies concerning the bacterial endosymbionts, since they oﬀer an excellent model to investigate important biological events, such as organelle evolution, genome reduction, and transfer of genetic information among host lineages. The BIOBITS goal is two-side: on the one hand, it pursues a logical data representation of genomic and proteomic components. On the other hand, it aims at the development of software modules allowing the user to retrieve and analyze data in a ﬂexible way.
Sat, 01 Jan 2011 00:00:00 GMThttp://hdl.handle.net/2318/914482011-01-01T00:00:00ZOn a Class of Reversible Primitive Recursive Functions and Its Turing-Complete Extensionshttp://hdl.handle.net/2318/1677880Titolo: On a Class of Reversible Primitive Recursive Functions and Its Turing-Complete Extensions
Abstract: Reversible computing is both forward and backward deterministic. This means that a uniquely determined step exists from the previous computational configuration (backward determinism) to the next one (forward determinism) and vice versa. We present the reversible primitive recursive functions (RPRF), a class of reversible (endo-)functions over natural numbers which allows to capture interesting extensional aspects of reversible computation in a formalism quite close to that of classical primitive recursive functions. The class RPRF can express bijections over integers (not only natural numbers), is expressive enough to admit an embedding of the primitive recursive functions and, of course, its evaluation is effective. We also extend RPRF to obtain a new class of functions which are effective and Turing complete, and represent all Kleene’s μ-recursive functions. Finally, we consider reversible recursion schemes that lead outside the reversible endo-functions.
Mon, 01 Jan 2018 00:00:00 GMThttp://hdl.handle.net/2318/16778802018-01-01T00:00:00ZA deep inference system with a self-dual binder which is complete for linear lambda calculushttp://hdl.handle.net/2318/151481Titolo: A deep inference system with a self-dual binder which is complete for linear lambda calculus
Abstract: We recall that SBV, a proof system developed under the methodology of deep inference, extends multiplicative linear logic with the self-dual non-commutative logical operator Seq. We introduce SBVB that extends SBV by adding the self-dual binder Sdb on names. The system SBVB is consistent because we prove that (the analogous of) cut-elimination holds for it. Moreover, the resulting interplay between Seq and Sdb can model β-reduction of linear λ-calculus inside the cut-free subsystem BVB of SBVB. The long-term aim is to keep developing a programme whose goal is to give pure logical accounts of computational primitives under the proof-search-as-computation analogy, by means of minimal and incremental extensions of SBV.
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/2318/1514812014-01-01T00:00:00Z