Related papers: Call-by-name Gradual Type Theory
We present a logically principled foundation for systematizing, in a way that works with any computational effect and evaluation order, SMT constraint generation seen in refinement type systems for functional programming languages. By…
The class of Basic Feasible Functionals BFF$_2$ is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a…
Global-type formalisms enable to describe the overall behaviour of distributed systems and at the same time to enforce safety properties for communications between system components. Our goal is that of amending a weakness of such…
The gradual guarantee is an important litmus test for gradually typed languages, that is, languages that enable a mixture of static and dynamic typing. The gradual guarantee states that changing the precision of a type annotation does not…
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no…
Automata learning is a technique that has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata…
In a recent paper we introduced a new framework for the study of call by need computations to normal form and root-stable form in term rewriting. Using elementary tree automata techniques and ground tree transducers we obtained simple…
Causal discovery from observational data is a challenging task that can only be solved up to a set of equivalent solutions, called an equivalence class. Such classes, which are often large in size, encode uncertainties about the orientation…
Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic code, several static analyses and type systems have been…
We classify programming languages according to evaluation order: each language fixes one evaluation order as the default, making it transparent to program in that evaluation order, and troublesome to program in the other. This paper…
Recent literature highlights the advantages of implementing social rules via dynamic game forms. We characterize when truth-telling remains a dominant strategy in gradual mechanisms implementing strategy-proof social rules, where agents…
This paper outlines a general formal framework for reasoning systems, intended to support future analysis of inference architectures across domains. We model reasoning systems as structured tuples comprising phenomena, explanation space,…
Scala's type system unifies ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new foundation for Scala and similar languages. Unfortunately, it is not clear…
In this work we describe preferential Description Logics of typicality, a nonmonotonic extension of standard Description Logics by means of a typicality operator T allowing to extend a knowledge base with inclusions of the form T(C) v D,…
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving with intensional type theories, with PVS being a notable…
This technical report investigates Kripke-style modal type theories, both simply typed and dependently typed. We examine basic meta-theories of the type theories, develop their substitution calculi, and give normalization by evaluation…
Prototypical Learning is based on the idea that there is a point (which we call prototype) around which the embeddings of a class are clustered. It has shown promising results in scenarios with little labeled data or to design explainable…
Contextual type theory distinguishes between bound variables and meta-variables to write potentially incomplete terms in the presence of binders. It has found good use as a framework for concise explanations of higher-order unification,…
The formal system lambda-delta is a typed lambda calculus that pursues the unification of terms, types, environments and contexts as the main goal. lambda-delta takes some features from the Automath-related lambda calculi and some from the…
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…