Related papers: A type system for Continuation Calculus

Gradual typing is an approach to integrating static and dynamic typing within the same language, and puts the programmer in control of which regions of code are type checked at compile-time and which are type checked at run-time. In this…

Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to…

This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of…

Destination passing -- aka. out parameters -- is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional…

It is common practice to compare the computational power of different models of computation. For example, the recursive functions are strictly more powerful than the primitive recursive functions, because the latter are a proper subset of…

Jay and Given-Wilson have recently introduced the Factorisation (or SF-) calculus as a minimal fundamental model of intensional computation. It is a combinatory calculus containing a special combinator, F, which is able to examine the…

Factorization -- a simple form of standardization -- is concerned with reduction strategies, i.e. how a result is computed. We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which…

We define a class of computable functions over real numbers using functional schemes similar to the class of primitive and partial recursive functions defined by G\"odel and Kleene. We show that this class of functions can also be…

Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile channels, a la pi-calculus. Its construction builds on a recent propositions as types correspondence between…

We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent…

In the calculus of dependent lambda eliminations (CDLE), it is possible to define inductive datatypes via lambda encodings that feature constant-time destructors and a course-of-values induction scheme. This paper begins to address the…

There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous - the latter is required to do any serious mathematics. We…

The logic FO(ID) uses ideas from the field of logic programming to extend first order logic with non-monotone inductive definitions. Such logic formally extends logic programming, abductive logic programming and datalog, and thus formalizes…

We introduce a type and effect system, for an imperative object calculus, which infers "sharing" possibly introduced by the evaluation of an expression, represented as an equivalence relation among its free variables. This direct…

Inductive definitions are an important form of knowledge. The logic FO(ID) is an extension of classical first-order logic FO with general non-monotone inductive definitions. Most existing proof systems for inductive definitions impose…

We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally…

Basic proof-search tactics in logic and type theory can be seen as the root-first applications of rules in an appropriate sequent calculus, preferably without the redundancies generated by permutation of rules. This paper addresses the…

Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies.…

Type systems usually characterize the shape of values but not their free variables. However, there are many desirable safety properties one could guarantee if one could track how references can escape. For example, one may implement…

Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the…