Related papers: Semantic Bound and Multi Types, Revisited
We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic…
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.
We provide a characterisation of strongly normalising terms of the lambda-mu-calculus by means of a type system that uses intersection and product types. The presence of the latter and a restricted use of the type omega enable us to…
This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the lambda-calculus. Recently, Accattoli et al. proposed a form of call-by-value strong evaluation for the lambda-calculus, the…
We illustrate the use of intersection types as a semantic tool for showing properties of the lattice of lambda theories. Relying on the notion of easy intersection type theory we successfully build a filter model in which the interpretation…
In this paper we invite the reader to a journey through three lambda calculi with resource control: the lambda calculus, the sequent lambda calculus, and the lambda calculus with explicit substitution. All three calculi enable explicit…
We investigate the possibility of a semantic account of the execution time (i.e. the number of \beta_v-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's call-by-value {\lambda}-calculus. For…
Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide…
This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably,…
We propose an intersection type system for an imperative lambda-calculus based on a state monad and equipped with algebraic operations to read and write to the store. The system is derived by solving a suitable domain equation in the…
A type assignment system for lambda-calculus enjoys the principal typing property if every typable term M has a special typing, called principal, from which all typings for M can be obtained via suitable operations. The existence of…
The good properties of Plotkin's call-by-value lambda-calculus crucially rely on the restriction to weak evaluation and closed terms. Open call-by-value is the more general setting where evaluation is weak but terms may be open. Such an…
We study a dependently typed extension of a multi-stage programming language \`a la MetaOCaml, which supports quasi-quotation and cross-stage persistence for manipulation of code fragments as first-class values and an evaluation construct…
We advocate the use of de Bruijn's universal abstraction $\lambda^\infty$ for the quantification of schematic variables in the predicative setting and we present a typed $\lambda$-calculus featuring the quantifier $\lambda^\infty$…
It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems rely on semantical techniques. In this work, we study…
This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed lambda-calculus. The proposed…
We consider the call-by-value lambda-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic and non-idempotent…
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…
We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard…
The Functional Machine Calculus (FMC, Heijltjes 2022) extends the lambda-calculus with the computational effects of global mutable store, input/output, and probabilistic choice while maintaining confluent reduction and simply-typed strong…