ﻻ يوجد ملخص باللغة العربية
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.
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
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
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 i
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
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.