ABSTRACT. In this work, we describe a presentation of dependent type systems rooted in bidirectional ideas, carefully separating at the syntax level between inferring and checking terms. This leads to a system which requires exactly the annotations needed to decide type-checking. Moreover, it readily embeds the two most usual ways to handle typing in dependent type systems, either by restricting to a certain subclass of terms that do not need annotations (as done in Agda), or by demanding certain annotations to be provided (as done in Coq), providing an elegant unifying framework.

ABSTRACT. Dependently-typed languages proved to be very useful for for statically enforcing properties of programs and for enabling type-driven development. However their implementations have been studied to a smaller extent than their theoretical properties. Theoretical models of these languages do not consider the plethora of features that exist in a bigger language like Agda, leading to issues in the implementation of the unifier and the elaborator. We present work-in-progress on a new design for elaboration of dependently-typed languages based on the idea of an open datatype for constraints to tackle these issues. This allows for a more compact base elaborator implementation while enabling extensions to the type system. We do not require modifications to the core of type-checker, therefore preserving safety of the language.

ABSTRACT. We introduce a mechanism of sort-polymorphism in type theory.

ABSTRACT. Main result (proof WIP): The type system for Degrees of Relatedness (a multimode system with modalities for parametricity, irrelevance and more) is (under conditions) the internal language of a lax-idempotent 2-monad (such as PSh, modulo strictification) iteratively applied to a single category. In particular, it can be seen as a modal system for multilevel type theory.

ABSTRACT. In this work we investigate how much type theories are able to prove about the natural numbers. We show that strong versions of type theory (both predicative and impredicative) prove exactly the same arithmetical formulas as Higher-order Heyting Arithmatic (HAH). As a consequence, we see that these versions are equiconsistent with HAH. Along the way, we investigate the different interpretations of higher-order logic in type theory, and to what extend dependent type theories can be seen as extensions of higher-order logic. In particular, we show that versions of the Calculus of Inductive Constructions and Martin-Löf type theory are conservative over HAH.

ABSTRACT. Enriched categories have found numerous applications, including effects in programming languages, abstract homotopy theory, and in higher category theory. In this abstract, we discuss an ongoing formalization of enriched categories in univalent foundations. More specifically, we define the notion of univalence for enriched categories, and we prove that the bicategory of univalent enriched category is univalent. This gives us a structure identity principle for enriched categories. The definitions and theorems in this abstract are formalized in the Coq proof assistant using the UniMath library \cite{UniMath}.

ABSTRACT. Sangiorgi's normal form bisimilarity is call-by-name, identifies all the call-by-name meaningless terms, and rests on open terms in its definition. The literature contains a normal form bisimilarity for the call-by-value λ-calculus, Lassen's enf bisimilarity, which validates all of Moggi's monadic laws. The starting point of this work is the observation that enf bisimilarity is not the call-by-value equivalent of Sangiorgi's, because it does not identify the call-by-value meaningless terms. The issue has to do with open terms. We then develop a new call-by-value normal form bisimilarity, deemed net bisimilarity, by exploiting an existing formalism for dealing with open terms in call-by-value. It turns out that enf and net bisimilarities are incomparable, as net bisimilarity identifies meaningless terms but it does not validate Moggi's laws. Moreover, there is no easy way to merge them. To better understand the situation, we provide a detailed analysis of the rich range of possible call-by-value normal form bisimilarities, relating them to Ehrhard's call-by-value relational semantics seen as a system of intersection types.

ABSTRACT. In our previous work, the embeddings of intuitionistic logic into modal logic S4 attributed to Girard and Goedel were show to obtain a unification of the call-by-name (cbn) and call-by-value (cbv) paradigms by the call-by-box paradigm existing in the box-calculus, which is a very simple extension of lambda calculus with a necessity (box) modality. In this work we study the instantiation of the box-calculus into call-by-push-value (cbpv), that is, the interpretation of the mentioned modality as the composition FU, with F and U the type operations of cbpv shifting between value and computation types. Levy's interpretations of cbn and cbv into cbpv factor through the mentioned instantiation. For this reason, we may say that, at the level of syntax and operational semantics, the unification achieved by cbpv is already obtained by call-by-box.

ABSTRACT. The idea of functional reactive programming (FRP) is to introduce abstractions that allow reactive programs to be represented in functional programming languages as functions on a type of signals. To ensure causality, productivity and other basic desirable properties of programs, one can use modal types to encode a notion of time step. Previous suggestions for modal FRP languages have used a modality corresponding to a global notion of time. This talk presents a new language for modal FRP centered around a new modality for asynchronous delay.

ABSTRACT. In this work I introduce CompLF (Computational Logical Framework), a framework suitable for defining computational type theories, that is, those whose definitional equality is purely generated by rewrite rules. It aims both at representing the syntax of type theories in a faithful way, and at being suitable for implementation. In order to make possible the latter, I also propose a theory-agnostic bidirectional typing algorithm.

ABSTRACT. We present ongoing work on a type-theoretic formulation of the state of the art on containers, including a Cubical Agda formalisation of generalised containers.

ABSTRACT. We report on a mechanization in the Coq proof assistant of the decidability of conversion and type-checking for Martin-Löf Type Theory (MLTT), extending a previous formalization in Agda. Our development proves the decidability not only of conversion, but also of type-checking, using bidirectional derivations that are canonical for typing. Moreover, we wish to narrow the gap between the object theory we formalize (currently MLTT with Π, Σ, natural numbers and one universe) and the metatheory used to prove the normalization result, e.g. MLTT, to a mere difference of universe levels. We thus avoid induction-recursion or impredicativity, which are central in previous work. Working in Coq, we also investigate how its features, including universe polymorphism and the metaprogramming facilities provided by tactics, impact the development of the formalization compared to the development style in Agda. The development is freely accessible on GitHub.

ABSTRACT. Multimode type theory (MTT) is parametrized by a mode theory: a 2-category whose objects, morphisms and 2-cells serve as internal modes, modalities and 2-cells. So far, this mode theory has remained in the metatheory, with syntactic modal type and term formers being indexed by metatheoretic gadgets. Building a syntactic lock calculus on top of the mode theory has several advantages: the modal aspects of substitution take the form of more familiar syntactical substitutions, the lock operation on contexts can be axiomatized as pseudofunctorial so that models of MTT no longer need to be strict(ified), and we can have internal mode, modality and 2-cell polymorphism with intensional 2-cell equality.

ABSTRACT. We study epimorphisms and acyclic types in univalent type theory, also known as homotopy type theory or univalent foundations (HoTT/UF).

ABSTRACT. In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. We have formalised all our results in Agda.

ABSTRACT. We present a generalization of Spector's bar recursion to the Diller-Nahm variant of Gödel's Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an interpretation to the double-negation shift principle. The interpretation is presented in a fully computational way, implementing sets via lists. We also present a demand-driven version of this extended bar recursion manipulating partial sequences rather than initial segments. We explain why in a Diller-Nahm context there seems to be several versions of this demand-driven bar recursion, but no canonical one.

ABSTRACT. Markov’s principle (MP) is an axiom from constructive mathematics, stating that Σ1 propositions (i.e. existential quantification over a decidable predicate on N) are stable under double negation. However, there are various non-equivalent definitions of decidable predicates and thus Σ^0_1 in constructive foundations, leading to non-equivalent Markov’s principles. This fact is often overlooked and leads to confusion: At the time of writing, both Wikipedia and nlab claim propositions to be equivalent to MP, which are however only respectively equivalent to two non-equivalent forms of MP.

We give three variants of MP in constructive type theory, along with respective equivalence proofs to different formulations of Post’s theorem (“Σ^0_1 -predicates with complement in Σ^0_1 are decidable”), stability of termination of computations, the statement that an extended natural number is finite if it is not infinite, and to completeness of natural deduction w.r.t. Tarski semantics over the (∀, →, ⊥)-fragment of classical first-order logic for Σ^0_1-theories. The first definition (MP_Prop) uses a purely logical definition of Σ^0_1 for predicates nat -> Prop, while the second one (MP_bool) relies on type-theoretic functions nat -> bool, and the third one (MP_PR) on a model of computation.

We conclude with the – to the best of our knowledge – first proof that MP_bool is not equivalent to MP_PR using a model via Cohen and Rahli’s TTC , and pose the open question how to separate MP_Prop from MP_bool – where the model would have to invalidate unique choice.