Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userIntersection Types for the Computational lambda-Calculus
96
0
0.0
(
0
)
Added by
Riccardo Treglia
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We study polymorphic type assignment systems for untyped lambda-calculi with effects, based on Moggis monadic approach. Moving from the abstract definition of monads, we introduce a version of the call-by-value computational lambda-calculus based on Wadlers variant with unit and bind combinators, and without let. We define a notion of reduction for the calculus and prove it confluent, and also we relate our calculus to the original work by Moggi showing that his untyped metalanguage can be interpreted and simulated in our calculus. We then introduce an intersection type system inspired to Barendregt, Coppo and Dezani system for ordinary untyped lambda-calculus, establishing type invariance under conversion, and provide models of the calculus via inverse limit and filter model constructions and relate them. We prove soundness and completeness of the type system, together with subject reduction and expansion properties. Finally, we introduce a notion of convergence, which is precisely related to reduction, and characterize convergent terms via their types.
rate research
Read More
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with Lob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Ruttens behavioural differential equations.
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).
We give a categorical semantics for a call-by-value linear lambda calculus. Such a lambda calculus was used by Selinger and Valiron as the backbone of a functional programming language for quantum computation. One feature of this lambda calculus is its linear type system, which includes a duplicability operator ! as in linear logic. Another main feature is its call-by-value reduction strategy, together with a side-effect to model probabilistic measurements. The ! operator gives rise to a comonad, as in the linear logic models of Seely, Bierman, and Benton. The side-effects give rise to a monad, as in Moggis computational lambda calculus. It is this combination of a monad and a comonad that makes the present paper interesting. We show that our categorical semantics is sound and complete.
The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the logic is not standard. Between all the logics that have been proposed as its foundation, we consider ISL, which gives a logical interpretation of the intersection by splitting the intuitionistic conjunction into two connectives, with a local and global behaviour respectively, being the intersection the local one. We think ISL is a logic interesting by itself, and in order to support this claim we give a sequent calculus formulation of it, and we prove that it enjoys the cut elimination property.
Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
