Working group Pole Proofs, programs and systems Thematic team Proofs and programs Manage talks Type theory and realisability Day, hour and place Wednesday at 2pm, room 1007 The calendar of events (iCal format). In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link. Contact(s) Hugo Herbelin Paul-André Melliès Previous talks Year 2023 Type theory and realisability Tuesday July 18, 2023, 2PM, Salle 147 (bâtiment Olympe de Gouge) Paige North (Utrecht University) Coinductive control of inductive data types In classical programming language theory, characterizing data types as initial algebras of an endofunctor that represents a specification of the data types is an important tool. In this work, we observe that the category of algebras of such an endofunctor is often enriched in its category of coalgebras. This enrichment carries strictly more information than the traditional, unenriched category. For example, when considering the endofunctor whose initial algebra is the natural numbers, we find that the enrichment encodes a notion of `partial' homomorphism, while the unenriched category encodes only `total' homomorphisms. We can also leverage this extra information to generalize the notion of initial algebras, following the theory of weighted limits. Year 2022 Type theory and realisability Wednesday December 14, 2022, 2PM, Salle 1007 Rémy Cerda (Institut de Mathématiques de Marseille, Université Aix-Marseille) To be announced. Type theory and realisability Wednesday November 16, 2022, 2PM, Salle 1007 Hugo Férée Et Sam Van Gool A formally verified construction of propositional quantifiers for intuitionistic logic A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC) - this result is commonly known as the uniform interpolation theorem for IPC. We recently completed a formalization of Pitts' result in the Coq proof assistant, and thus a verified implementation of the propositional quantifiers. Our Coq formalization in addition allowed us to extract an OCaml program that computes propositional formulas that realize intuitionistic versions of ∃p φ and ∀p φ from p and φ, and runs quickly on examples. In this talk, we will give some background for the result, and I will make some points about its proof that we clarified during its implementation, which also give some new insights about the “pen-and-paper” proof. In our implementation, as in Pitts' original proof, the propositional quantifiers are defined by a mutual induction based on Dyckhoff's proof calculus LJT. The correctness of the construction is then proved by an induction on the size of an LJT-proof. The techniques used and lessons learned from our implementation may also be of more general interest for verified implementations of other proof-theoretic results. Type theory and realisability Friday October 21, 2022, 10AM, Salle 1007 Thorsten Altenkirch Do we need classical logic? How should we make sense of the fact that classical mathematics officially is based on ZFC, but people that formalize classical mathematics in the computer use a foundation different from ZFC, e.g. type theory in the case of Lean ormalization? Type theory and realisability Wednesday October 19, 2022, 2PM, Salle 1007 Peter Dybjer On Generalized Algebraic Theories and Categories with Families We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwF_Σ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwF_Σ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Lo ̈f type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs. Also on https://galene.org:8443/group/herbelin/gt-rea-tt (no password) Type theory and realisability Wednesday October 19, 2022, 3:15PM, Salle 1007 Ambrus Kaposi Formalisation of type theory in type theory using quotient-inductive-inductive-recursive types In 2006, Nils Anders Danielsson formalised type theory in Agda using inductive-inductive-recursive types (IIRTs) before those types were understood. In 2009, James Chapman formalised type theory in Agda using inductive-inductive types (IITs) before the term “induction-induction” was coined. In 2016, Thorsten and I formalised type theory in Agda using quotient inductive-inductive types (QIITs) before a formal definition of QIITs was given. Cubical Agda now supports quotient inductive-inductive-recursive types (QIIRTs). We don't yet understand QIIRTs, so it is time to formalise the syntax of type theory using them! This is work in progress. Also on https://galene.org:8443/group/herbelin/gt-rea-tt (no password) Type theory and realisability Wednesday October 12, 2022, 2PM, Salle 3052 Félix Castro An interpretation (by parametricity) of E-HA^ω inside HA^ω HA^ω (Higher Type Arithmetic) is a first order many sorted theory. It is a conservative extension of HA (Heyting Arithmetic a.k.a the intuitionistic version of Peano Arithmetic) obtained by extending the syntax of terms to all the System T : the objects of interest here are the functionals of “higher types”. While equality between natural numbers is well understood (it is canonical and decidable), how equality between functionals can be defined ? From this question, different versions of HA^ω arise : an extensional version (E-HA^ω) and an intentional version (I-HA^ω). In this talk, we will see how the study of a (family of) partial equivalence relation(s indexed by the sorts of System T) leads us to design a translation (by parametricity) from E-HA^ω (HA^ω + extensional equality at all level) to HA^ω (where equality is only defined on natural numbers). Type theory and realisability Wednesday July 6, 2022, 2PM, Salle 1007 James Lipton (Wesleyan Univ., USA) CUT ELIMINATION in Higher-Order with (HO) constraints We will present a system of Intensional Higher-Order Intuitionistic Logic with Higher-Order Saraswat Constraints, hoI(C). The Logic and its variants were developed by Artalejo, Nieva, Leach (Madrid), and subsequently by Lipton, Nieva and Hermant, the original aim being to add constraints to a lambda-Prolog style language. If constraints are unrestricted, cut-elimination is easily shown to fail, because of the way the system handles equality rules. Our work studies conditions on the constraint system C that guarantee cut-elimination. The techniques used are based on Takahashi, Prawitz ande Andrews' work in classical type theory, Lipton and DeMarco for intuitionistic type theory, with ideas developed by Hermant for Logique Modulo, Hermant and Lipton for Logic with sequent axioms, as well as cut-elimination techniques due to Okada and Maehara. We will briefly discuss Kripke and HA semantics for these calculi, with some remarks on fibrational semantics developed by the speaker with Gianluca Amato (Pescara, Italy) if time permits! This will be a blackboard talk (with maybe a few slides) and will include work in progress! Year 2021 Type theory and realisability Wednesday December 8, 2021, 2PM, Salle 1007 Federico Olimpieri (Université de Leeds) Categorifying Intersection Types We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction. Type theory and realisability Wednesday February 24, 2021, 2PM, online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7) Elaine Pimentel (UFRN - Brazil) On linear logic, modalities and frameworks We start by presenting a local system for linear logic (LL) based on linear nested sequents. Relying on that system, we propose a general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine, bounded and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. We then move to the question of giving an interpretation to subexponentials. We will show a game interpretation of affine linear logic with subexponentials, viewing the game as a playground for illuminating semantic intuitions underlying resource conscious reasoning. Interestingly enough, this led to the proposal of new sequent systems for capturing the notions of costs and budget in a fragment of linear logic with subexponentials, thus opening new possibilities for analysing the problem of comparing proofs. We finish the talk by showing a computational interpretation of subexponentials in the process-as-formula fashion, where process constructors are mapped to logical connectives and computational steps are related to proof steps. In particular, we will show in detail the role of pre-orders in subexponentials for the adequate specification of different modalities in concurrent systems, such as time, space, epistemic and preferences. We end with a discussion about which new models of computation should arise from the extension of the concept of modality in linear logic. Year 2020 Type theory and realisability Wednesday December 16, 2020, 2:30PM, Online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7) Pierre Pradic (University of Oxford) Implicit automata in λ-calculi The talk will be based on joint work with Lê Thành Dũng (Tito) Nguyễn (https://arxiv.org/pdf/2008.01050.pdf). This work is part of an exploration of the expressiveness of the simply-typed λ-calculus (STLC) and related substructural variants (linear, affine, planar) using Church encodings of datatypes. More specifically, we are interested in the connection with automata theory for string transductions and languages. After introducing and motivating the problems using Hillebrand and Kanellakis' result stating that the classes of STLC-definable and regular languages coincide, I will discuss refinements we obtained for linear λ-calculi. I will focus on a correspondence with functions computed by copyless streaming string transducers (SSTs), and particularly on the ingredients of a completeness proof translating λ-terms to transducers. This will involve the notions of categorical automata as introduced by Colcombet and Petrisan, categorical models of linear logic and free completions, as well as automata-theoretic techniques related to the composition and determinization of SSTs. Type theory and realisability Monday December 14, 2020, 2PM, Online (https://bbb-front.math.univ-paris-diderot.fr/recherche/hug-a7x-lga-hy7) Armaël Guéneau (Aarhus University) Mechanized Program Verification on a Capability Machine in the Presence of Untrusted Code A capability machine is a kind of CPU which supports fine-grained privilege separation using capabilities (a pointer carrying a certain amount of authority). In this talk, I will present a methodology for verifying the functional correctness of capability machine programs that call (or are called by) unknown and potentially malicious code. The key aspects to the approach is a program logic for reasoning about known code, and a logical relation which provides a specification for unknown code. I will then hint at how we extend this methodology to reason about a secure calling convention enforcing a secure stack policy and the well-bracketedness of function calls. This work has been entirely mechanized in Coq using the Iris framework: https://github.com/logsem/cerise https://github.com/logsem/cerise-stack Year 2019 Type theory and realisability Wednesday December 11, 2019, 2PM, Salle 1007 Danny Gratzer Type Theory à la Mode Modalities have proved to be a recurring phenomenon in type theories, arising in both mathematical and computational contexts. For instance, recent work on cubical type theory has simplified the construction of univalent universes using the internal type theory of cubical sets supplemented with a comonad. On the other hand, guarded type theory has provided an account of coinduction using a handful of modalities. Despite the wide variety of uses, a general framework for modal dependent type theories has still proven elusive. Each modal situation requires a handcrafted type theory, and establishing the properties of these type theories requires a significant technical investment. In this work, we have attempted to isolate a class of modal situations which can be given a single uniform syntax and allow for the typical metatheorems of type theory to be proven once and for all. Our calculus takes a mode theory as a parameter (an abstract description of the collection of modes, the modalities between them, and the ways in which they interactions) and produces a full dependent type theory satisfying canonicity. Our approach generalizes the ideas latent in Nuyts, Vezzosi, and Devriese, and simplifies the forthcoming work by Licata, Shulman, and Riley on a subset of mode theories. This calculus is sufficiently flexible to model internal parametricity, guarded recursion, and even axiomatic cohesion. Type theory and realisability Wednesday November 27, 2019, 2PM, Salle 1007 Bas Spitters (Aarhus university) Synthetic topology in Homotopy Type Theory for probabilistic programming The ALEA Coq library formalizes measure theory based on a variant of the Giry monad on the category of sets. This enables the interpretation of a probabilistic programming language with primitives for sampling from discrete distributions. Continuous distributions (e.g. over the reals) cannot be treated this way, as not all subsets are measurable. We propose the use of synthetic topology to model continuous distributions while staying close to ALEA's approach. This allows us to model the apWhile language used in easycrypt to model differential privacy. We study the initial sigma-frame and the corresponding induced topology on arbitrary sets. We define valuations and lower integrals on sets that takes into account these intrinsic topologies, and we prove versions of the Riesz and Fubini theorems. We then show how the Lebesgue valuation, and hence continuous distributions, can be constructed. By interpreting our synthetic results in the K2-realizability topos, we recover the valuations on topological domains used as the semantics for the augurv2 probabilistic language, which has been used for machine learning. Joint work with Martin Bidlingmaier (Aarhus) and Florian Faissole (INRIA). Type theory and realisability Wednesday September 18, 2019, 2PM, Salle 1007 Karl Palmskog (The University of Texas at Austin) mCoq: Mutation Proving for Analysis of Verification Projects Mutation analysis, which introduces artificial defects into software systems, is the basis of mutation testing, a technique widely applied to evaluate and enhance the quality of test suites. However, despite the deep analogy between tests and formal proofs, mutation analysis has seldom been considered in the context of deductive verification. We propose mutation proving, a technique for analyzing verification projects that use proof assistants. We implemented our technique for the Coq proof assistant in a tool dubbed mCoq. mCoq applies a set of mutation operators to Coq definitions of functions and datatypes, inspired by operators previously proposed for functional programming languages. mCoq then checks proofs of lemmas affected by operator application. To make our technique feasible in practice, we implemented several optimizations in mCoq such as parallel proof checking. We applied mCoq to several medium and large scale Coq projects, and recorded whether proofs passed or failed when applying different mutation operators. We then qualitatively analyzed the mutants, and found several examples of weak and incomplete specifications. For our evaluation, we made many improvements to serialization of Coq code and even discovered a notable bug in Coq itself, all acknowledged by developers. We believe mCoq can be useful both to proof engineers for improving the quality of their verification projects and to researchers for evaluating proof engineering techniques. Joint work with Ahmet Celik, Marinela Parovic, Emilio Jésus Gallego Arias, and Milos Gligoric. Speaker bio: Karl Palmskog is a Research Fellow at The University of Texas at Austin. His research focuses on proof engineering techniques and verification of distributed systems using Coq. He was previously a postdoctoral researcher at University of Illinois at Urbana-Champaign, working on topics related to the actor model of message-passing concurrency. He obtained his PhD from KTH Royal Institute of Technology. Video available at https://youtu.be/S6b6OMFiDFA Slides available at https://setoid.com/slides/irif-2019.pdf Type theory and realisability Friday May 24, 2019, 2PM, Salle 1007 Hugo Moeneclaey Monoids up to Coherent Homotopy in Two-Level Type Theory When defining a monoid structure on an arbitrary type in HoTT, one should require a multiplication that is not only homotopy-associative, but also has an infinite tower of higher homotopies. For example in dimension two one should have a condition similar to Mac Lane’s pentagon for monoidal categories. We call such a monoid a monoid up to coherent homotopy. The goal of my internship in Stockholm was to formalize them in Agda. It is well-known that infinite towers of homotopies are hard to handle in plain HoTT, so we postulate a variant of two-level type theory, with a strict equality and an interval type. Then we adapt the set-theoretical treatment of monoids up to coherent homotopy using operads as presented by Clemens Berger and Ieke Moerdijk [1,2]. Our main results are: (a) Monoids up to coherent homotopy are invariant under homotopy equivalence (b) Loop spaces are monoids up to coherent homotopy. In this talk I will present the classical theory of monoids up to coherent homotopy, and indicates how two-level type theory can be used to formalize it. References 1. Axiomatic homotopy theory for operads (arxiv.org/abs/math/0206094) 2. The Boardman-Vogt resolution of operads in monoidal model categories (arxiv.org/abs/math/0502155) Organisé conjointement avec le groupe de travail catégories supérieures, polygraphes, et homotopie. Type theory and realisability Friday March 29, 2019, 11AM, Salle 3052 Emilio J. Gallego Arias (MINES ParisTech) Formalized Logic Programming, from Theory to Practice I will present past and ongoing work to develop mechanically-verified semantics and implementations of constraint logic programming. (Constraint) logic programming is based on the utilization of proof search as a device for computation. The power that such a paradigm offers often comes at a cost for formal language research and implementation. Logic variables, unification, renaming apart, and proof search strategies are cumbersome to handle formally, and often specified informally or at the meta-logical level. In the first part of the talk I will describe algebraic semantics for proof search, based on the Tarski's relation algebras and Freyd's allegories. The main idea is to translate logic programs to _variable free_ relations; distribute relational algebras with quasi-projections do interpret defined predicates, whereas first-order rewriting simulates the traditional SLD proof search procedure. While the relation-based approach suffices to capture the proof search in a complete way, some rewriting steps are unsatisfactory from a more operational point of view, as they introduce extraneous terms in order to preserve certain global constraints. In an attempt to remedy this, we switch to the categorical version of relation algebra: allegories. In particular, for a signature Σ, we will interpret logic programs in the so-called Σ-allegories: distribute allegories whose conjunctive part is tabulated by a “Regular Lawvere Category”. In this setting, the single primitive of relation composition emcompasses unification, garbage collection, parameter passing, and environment creation and destruction. Tabulations play a crucial role, with their domain representing the set of live existential variables. Proof search is carried out by a notion of diagram rewriting, and is complete w.r.t. SLD, and satisfactory as form of abstract syntax for the program's execution. This new semantics paves the way to a formal extension of CLP with useful programming constructs. In the second part, I will shift focus to a different part of the logic programming spectrum, and describe ongoing efforts on formalizing logic programming engines over theories with finitary models on the Coq proof assistant. In particular, I will describe the implementation and verification of an engine for incremental model computation of a subset of Datalog that we have dubbed “Regular Datalog”. “Regular” Datalog stems from [Reutter,Romero,Vardi] Regular Queries, and it is of interest to the graph database community. The finite nature of the semantics of such programs allows to handle them quite naturally inside a constructive proof assistant, and to remain close to the usual mathematical notation. Borrowing from techniques from incremental view maintenance, we have developed a verified incremental model construction engine; to achieve a cost-effective mechanized proof of the soundness of the engine we had to develop a few notions specific to the ITP domain, such as generalized program signatures and a notion of relative satisfaction. We provide some preliminary benchmarks of the verified engine over realistic scenarios. To conclude, I will present some challenges that the practical utilization of proof assistants does face these days, and briefly discuss my ongoing work on this area. Year 2018 Type theory and realisability Friday May 18, 2018, 11AM, Salle 3052 Raphaël Cauderlier Tactics and certificates in Meta Dedukti Tactics are often featured in proof assistants to simplify the interactive development of proofs by allowing domain-specific automation. Moreover, tactics are also helpful to check the output of automatic theorem provers because they can rebuild details that the provers omit. We use meta-programming to define a tactic language for the Dedukti logical framework which can be used both for checking certificates produced by automatic provers and for developing proofs interactively. More precisely, we propose a dependently-typed tactic language for first-order logic in Meta Dedukti and an untyped tactic language built on top of the typed one. We show the expressivity of these languages on two applications: a transfer tactic and a resolution certificate checker. Type theory and realisability Wednesday April 25, 2018, 2PM, Salle 1007 Hadrien Batmalle (IRIF) Préservation de propriétés du modèle de départ en réalisbilité classique La réalisabilité classique permet d'interpréter des théories mathématiques classiques, comme la théorie des ensembles ZF, dans divers modèles de calcul (lambda-calcul avec continuations, domaines…) axiomatisés au moyen d'algèbres de réalisabilité. Elle produit ainsi des modèles de ces théories, de même qu'une technique bien connue, le forcing de Cohen, dont elle est en fait une généralisation. Jusqu'ici, la réalisabilité classique a seulement été étudiée à partir d'un modèle de départ “raisonnable”, supposé au moins valider AC, voire même défini comme l'univers constructible. Dans cet exposé, on étudiera un analogue des “conditions d'antichaîne” du forcing nous permettant d'exporter certaines propriétés du modèle de départ au modèle de réalisabilité; et on l'appliquera pour obtenir des programmes réalisant Non DC (resp. Non CH) à partir de modèles de ZF bien choisis validant Non DC (resp. Non CH). — DC: axiome du choix dépendant CH: hypothèse du continu Type theory and realisability Monday March 19, 2018, 1:15PM, 3052 Adrien Guatto A Generalized Modality for Recursion Nakano’s later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infnite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale. Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limitations stem from the fact that the later modality is not expressive enough to capture precise input-output dependencies of functions. As a consequence, guarded type theories reject many productive definitions. Combining insights from guarded type theories and synchronous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behaved reindexing of the time scale to a type. We call such reindexings time warps. Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ours. We integrate our modality into a typed λ-calculus. We equip this calculus with an operational semantics, as well as an adequate denotational semantics in the topos of trees, a standard categorical model for guarded recursion. Building on top of categorical ideas, we describe an abstract type-checking algorithm whose completeness entails the coherence of both semantics. Attention, horaire et salle inhabituels Type theory and realisability Wednesday March 14, 2018, 2PM, Salle 1007 Laura Fontanella (Institut de Mathématiques de Marseille) L'Axiome du Choix dans la réalisabilité classique La réalisabilité fournit une interpretation des formules d'un système logique (ou d'une théorie) dans un modèle de calcul. Introduite par Kleene dans les années `40, la réalisabilité est née comme une interprétation des formules de l'arithmétique de Heyting par des ensembles d'indices de fonctions récursives. Avec J.-L. Krivine, la recherche en réalisabilité a évolué jusqu’à englober les axiomes de la théorie des ensembles. Les techniques développées par Krivine fournissent une méthode pour construire des modèles de la théorie des ensembles où tout énoncé de la théorie ZF plus l'Axiome du Choix Dépendant est réalisé. L'Axiome du Choix Dépendant, DC, est une version faible de l'Axiome du Choix; si et comment il serait possible de réaliser l'Axiome du Choix dans sa totalité reste une question ouverte. Nous allons considérer des principes intermédiaires: (1) le principe de partition, PP : étant donné deux ensembles A et B, s’il y a une surjection de A dans B, alors il y a une injection de B dans A; (2) le “Dual Cantor Bernstein theorem”, CB* : s’il y a une surjection de A dans B et une surjection de B dans A, alors A et B sont équipotents; (3) le principe de partition faible, WPP : s’il y a une surjection de A dans B et une injection de A dans B, alors A et B sont équipotents. Ces principes découlent de l'Axiome du Choix et sont plus forts que l'Axiome du Choix Dépendant. Cependant, on ne sait pas s'ils sont équivalents à l'Axiome du Choix et cela est un vieux problème ouvert formulé par B. Banacschewski et G. Moore en 1990. Est-il possible de construire un modèle de réalisabilité pour l'un de ces principes? Cette recherche peut aboutir à deux situations divergentes: soit on trouvera des modèles de réalisabilité pour ces principes où l’axiome du choix est également réalisé, soit on s’arrêtera à une étape donnée sur des modèles de réalisabilité où l’un de ces principes (ou tous) est réalisé, tandis que l’Axiome du Choix ne l’est pas, dans ce dernier cas on aurait alors montré que ces principes ne sont pas équivalents à l’Axiome du Choix et on aurait ainsi résolu le problème de Banacschewski-Moore. Je vous presenterai l'avancement de mes recherches dans ce domaine. Type theory and realisability Wednesday February 14, 2018, 2PM, Salle 1007 Jérôme Siméon (Clause, Inc.) Specifying and compiling domain specific languages using Coq: Three case studies Domain specific languages (DSL) can be well suited for certain business scenarios and be easier to learn for non-developers. We present our experience using the Coq proof assistant to support the formal specification and the compilation for three different DSLs: JRules (a language for business rules), SQL (a language for relational databases), and Jura (a language for legal contract). We describe how each of those languages comes with its own challenges, and how they benefit differently from the use of a proof assistant. We also show how we could exploit their commonalities to build an optimizing and (partially) verified compiler for each of them. The core of that compiler uses traditional database representations (the Nested Relational Algebra and its corresponding Calculus) for optimization and code-generation. – Some of this work was done jointly with Joshua Auerbach, Martin Hirzel, Louis Mandel and Avi Shinnar as part of the Q*cert project (https://querycert.github.io/). Type theory and realisability Wednesday January 31, 2018, 2PM, Salle 1007 Armaël Guéneau (Inria Paris) A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification I will present a framework for simultaneously verifying the functional correctness and the worst-case asymptotic time complexity of higher-order imperative programs. The framework is built on top of Separation Logic with Time Credits, embedded in the Coq proof assistant. I will formalize the O notation, which is key to enabling modular specifications and proofs, and cover the subtleties of the multivariate case, where the complexity of a program fragment depends on multiple parameters. I will propose a way of integrating complexity bounds into specifications, present lemmas and tactics that support a natural reasoning style, and illustrate their use with a collection of examples. Type theory and realisability Wednesday January 17, 2018, 2PM, Salle 1007 Rodolphe Lepigre Practical Curry-Style using Choice Operators, Local Subtyping and Circular proofs In a recent (submitted) work with Christophe Raffalli, we designed a rich type system for an extension of System F with subtyping. It includes primitive sums and products, existential types, (co-)inductive (sized) types, and it supports general recursion with termination checking. Despite its Curry-style nature, the system can be (and has been) implemented thanks to new techniques based on choice operators, local subtyping and circular proofs. During the talk, I will give you a flavour of these three ideas. In particular, I will show how choice operators can be used to get rid of free variables (and thus typing contexts), while yielding a clear semantics. I will show how local subtyping can be used to make the system syntax-directed. And I will show how circular proofs may be used to handle (co-)inductive types and (terminating) recursion. References and links: - paper: http://lepigre.fr/files/docs/lepigre2017_subml.pdf - implementation of the system: https://github.com/rlepigre/subml - online interpreter and examples: https://rlepigre.github.io/subml Year 2017 Type theory and realisability Wednesday December 20, 2017, 2PM, Salle 1007 Ludovic Patey (ICJ, Lyon) Introduction aux mathématiques à rebours Les mathématiques à rebours sont un domaine fondationnel qui vise à trouver les axiomes optimaux pour prouver les théorèmes de la vie de tous les jours. Elles se placent dans l'arithmétique du second ordre, avec une théorie de base, RCA, capturant informellement les “mathématiques calculables”. Nous reviendrons sur les justifications historiques des mathématiques à rebours, présenterons ses principales observations, ainsi que l'approche moderne des mathématiques à rebours comme formalisme de classification de phénomènes calculatoires. Type theory and realisability Wednesday December 6, 2017, 2PM, Salle 1007 Francesco A. Genco (IRIF - TU Wien) Typing Parallelism and communication through hypersequents We present a Curry–Howard correspondence for Gödel logic based on a simple natural deduction reformulating the hypersequent calculus for this logic. The resulting system extends simply typed λ-calculus by a symmetric higher-order communication mechanism between parallel processes. We discuss a normalisation procedure and several features of the parallel λ-calculus. Following A. Avron's 1991 thesis on the connection between hypersequents and parallelism, we also discuss the generalisation of the employed techniques for other intermediate logics. Type theory and realisability Wednesday November 29, 2017, 2PM, Salle 1007 Guilhem Jaber (ENS Lyon) A Trace Semantics for System F Parametric Polymorphism In this talk, we present a trace model for System F that captures Strachey parametric polymorphism. The model is built using operational nominal game semantics and enforces parametricity by using names. This model is used here to prove a conjecture of Abadi, Cardelli, Curien and Plotkin which states that Strachey equivalence implies Reynolds equivalence (i.e. relational parametricity) in System F. Type theory and realisability Thursday March 16, 2017, 2PM, Salle 1007 Pierre-Marie Pédrot An Effectful Way to Eliminate Addiction to Dependence We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory, such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin.