IRIS Uni Torinohttps://iris.unito.itIl sistema di repository digitale IRIS acquisisce, archivia, indicizza, conserva e rende accessibili prodotti digitali della ricerca.Thu, 14 Nov 2019 22:33:24 GMT2019-11-14T22:33:24Z10891Comparing Cubes of Typed and Type Assignment systemshttp://hdl.handle.net/2318/9566Titolo: Comparing Cubes of Typed and Type Assignment systems
Wed, 01 Jan 1997 00:00:00 GMThttp://hdl.handle.net/2318/95661997-01-01T00:00:00ZA Type Inference Algorithm for a complete stratification of the Polymorphic Type Disciplinehttp://hdl.handle.net/2318/9264Titolo: A Type Inference Algorithm for a complete stratification of the Polymorphic Type Discipline
Sat, 01 Jan 1994 00:00:00 GMThttp://hdl.handle.net/2318/92641994-01-01T00:00:00ZIntersection Typed Lambda-Calculushttp://hdl.handle.net/2318/9569Titolo: Intersection Typed Lambda-Calculus
Tue, 01 Jan 2002 00:00:00 GMThttp://hdl.handle.net/2318/95692002-01-01T00:00:00ZBounding normalization time through intersection typeshttp://hdl.handle.net/2318/140516Titolo: Bounding normalization time through intersection types
Tue, 01 Jan 2013 00:00:00 GMThttp://hdl.handle.net/2318/1405162013-01-01T00:00:00ZStandardization in resource lambda-calculushttp://hdl.handle.net/2318/140515Titolo: Standardization in resource lambda-calculus
Sun, 01 Jan 2012 00:00:00 GMThttp://hdl.handle.net/2318/1405152012-01-01T00:00:00ZPrincipal Type scheme and unification for intersection type disciplinehttp://hdl.handle.net/2318/9263Titolo: Principal Type scheme and unification for intersection type discipline
Fri, 01 Jan 1988 00:00:00 GMThttp://hdl.handle.net/2318/92631988-01-01T00:00:00ZPrincipal Typing in Elementary Affine Logichttp://hdl.handle.net/2318/9570Titolo: Principal Typing in Elementary Affine Logic
Wed, 01 Jan 2003 00:00:00 GMThttp://hdl.handle.net/2318/95702003-01-01T00:00:00ZThe Parametric Lambda-Calculus: a Metamodel for Computationhttp://hdl.handle.net/2318/16319Titolo: The Parametric Lambda-Calculus: a Metamodel for Computation
Abstract: The lambda-calculus was invented by Church in the 1930s with the purpose of supplying a logical foundation for logic and mathematics.
Its use by Kleene as a coding for computable functions makes it the first programming language, in an abstract sense, exactly as the Turing machine can be considered the first computer machine. The lambda-calculus has quite a simple syntax (with just three formation rules for terms) and a simple operational semantics (with just one operation, substitution), and so it is a very basic setting for studying computation properties.
The first contact between lambda-calculus and real programming languages was in the years 1956-1960, when McCarthy developed the LISP programming language, inspired from lambda-calculus, which is the first ``functional'' programming language, i.e., where functions are first-class citizens. But the use of lambda-calculus as an abstract paradigm for programming languages started later as the work of three important scientists: Strachey, Landin and Bøhm. Strachey used the lambda-notation as a descriptive tool to represent functional features in programming when he posed the basis for a formal semantics of programming languages. Landin formalized the idea that the semantics of a programming language can be given by translating it into a simpler language that is easier to understand. He identified such a target language in lambda-calculus and experimented with this idea by giving a complete translation of ALGOL60 into lambda-calculus.
Moreover, he declared that a programming language is nothing more than lambda-calculus plus some ``syntactic sugar''.
Bøhm was the first to use lambda-calculus as an effective programming language, defining, with Gross, the CUCH language, which is a mixture of lambda-calculus and the Curry combinators language, and showing how to represent in it the most common data structures.
But, until the end of the 1960s, lambda-calculus suffered from the lack of a formal semantics.
In fact, while it was possible to codify in it all the computable functions, the meaning of a generic lambda-term not related to this coding was unclear. The attempt to interpret lambda-terms as set-theoretic functions failed, since it would have been necessary to interpret it into a set D isomorphic to the set of functions from D to D, which is impossible since the two spaces always have different cardinality. Scott solved the problem by interpreting lambda-calculus in a lattice isomorphic to the space of its continuous functions, thus giving it a clear mathematical interpretation. So the technique of interpretation by translation, first developed by Landin, became a standard tool to study the denotational semantics of programming languages; almost all textbooks in denotational semantics follow this approach.
But there was a gap between lambda-calculus and the real functional programming languages. The majority of real functional languages have a ``call-by-value'' parameter passing policy, i.e., parameters are evaluated before being passed to a function, while the reduction rule of lambda-calculus reflects a ``call-by-name'' policy, i.e., a policy where parameters are passed without being evaluated. In the folklore there was the idea that a call-by-value behaviour could be mimicked in lambda-calculus just by defining a suitable reduction strategy. Plotkin proved that this intuition was wrong and that lambda-calculus is intrinsically call-by-name. So, in order to describe the call-by-value evaluation, he proposed a different calculus, which has the same syntax as lambda-calculus, but a different reduction rule.
The aim of this book is to introduce both the call-by-name and the call-by-value lambda-calculi and to study their syntactical and semantical properties, on which their status of paradigmatic programming languages is based. In order to study them in a uniform way we present a new calculus, the lambda-Delta-calculus, whose reduction rule is parametric with respect to a subset Delta of terms (called the set of input values) that enjoy some suitable conditions.Different choices of Delta allow us to define different languages, in particular the two lambda-calculus variants we are speaking about. The most interesting feature of lambda-Delta-calculus is that it is possible to prove important properties (like confluence) for a large class of languages in just one step. We think that lambda-Delta-calculus can be seen as the foundation of functional programming.
Thu, 01 Jan 2004 00:00:00 GMThttp://hdl.handle.net/2318/163192004-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:00ZCharacterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculushttp://hdl.handle.net/2318/151509Titolo: Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-Calculus
Wed, 01 Jan 2014 00:00:00 GMThttp://hdl.handle.net/2318/1515092014-01-01T00:00:00Z