The Löwenheim-Skolem (LS) theorem is a central result about first-order logic, entailing that the formalism is incapable of distinguishing different infinite cardinalities. In particular its so-called downward part (DLS), stating that every infinite model can be turned into a countably infinite model with otherwise the exact same behaviour, can be considered surprising or even paradoxical. Therefore the exact assumptions under which the downward Löwenheim-Skolem (DLS) theorem applies have been analysed thoroughly: From the perspective of (classical) reverse mathematics, the DLS theorem is equivalent to the dependent choice axiom (DC), a weak form of the axiom of choice, stating that there is a path through every total relation.

An even more informative answer, taking into account the computational content, can be obtained by the perspective of constructive reverse mathematics. This programme is concerned with the analysis of logical strength over a constructive meta-theory, i.e. in particular without the law of excluded middle (LEM), stating that p ∨ ¬p for all propositions p, and ideally also without countable choice (CC), a consequence of DC. In that setting, finer logical distinctions become visible and thus one can investigate whether (1) the DLS theorem still follows from DC alone, without any contribution of LEM, and (2) whether it still implies the full strength of DC, without any contribution of CC. We show that neither (1) nor (2) is the case by observing that the DLS theorem requires a fragment of LEM, which we call the blurred drinker paradox, and that it implies only a similarly blurred fragment of DC.

Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions. In the examples, equivalence of structures in various fragments of infinitary first-order logic can be captured by transferring bisimilarity along the adjunction. In most applications, the categories involved are locally finitely presentable and the adjunctions finitely accessible. Drawing on this insight, we identify the expressive power of this class of adjunctions. We show that the ranks of back-and-forth games in the arboreal category are definable by formulae à la Hintikka. Thus, the relation between extensional objects induced by bisimilarity is always coarser than equivalence in infinitary first-order logic. Our approach relies on Gabriel-Ulmer duality for locally finitely presentable categories, and Hodges’ word-constructions.

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.

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.

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?

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.

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.

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).

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!

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.

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.

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.

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

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.

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).

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.

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)

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.

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.

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

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.

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.

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/).

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.

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

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.

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.

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.

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.