Gallinette Xmas Type Theory Fest 2023

After Enzo Crance's PhD thesis and before Martin Baillon's one, we will have the pleasure to host a special event on December 20th 2023, in room 3, ground floor of Building 11 (the oldest part of the compute science laboratory).

There will be a departure from cafeteria in Building 34 at 9.50AM.


Program

  • 9.30AM: Welcome (Cafeteria, 4th floor of building 34)
  • 10.00: Ambrus Kaposi -- Internal parametricity, without an interval
    In this talk I will describe a baby version of higher observational type theory. This theory has internal parametricity: it is provable that Church-encoded natural numbers satisfy induction (up to universe size issues). Compared to previous type theories with internal parametricity, there is no built-in geometry (interval) in its syntax or operations mentioning arbitrary dimensions. It is a simple extension of Martin-Löf's type theory with a few new operations and equations. It can be described using second-order abstract syntax/logical framework, thus it is a non-substructural theory. It is modelled by presheaves on semicartesian cubes, the same cube category on top of which the first constructive model of univalence was built (cubical type theories are based on cube categories with more structure, i.e. De Morgan or cartesian). I will prove that this type theory satisfies canonicity, that is, every closed boolean computes to either true or false. This is joint work with Thorsten Altenkirch, Yorgo Chamoun and Michael Shulman.
  • 11:00: Break
  • 11.10: Enrico Tassi -- Elpi: the language you already know without knowing it
    Elpi is the programming language of "inference rules" which I bet everybody used at least once in his/her papers. We give a short introduction to the language and use it to implement W, the algorithm assigning types to Standard ML terms. We conclude by discussing its application to the Coq proof assistant and identifying its strong (and weak) points.
  • 12.10 End of the morning session.

  • 14.30: Andrej Bauer --The countable reals.
    We define a new kind of realizability, called parameterized realizability, and use it do construct a topos in which the Dedekind reals are countable. The construction relies on an ingeneous application of Kakutani’s fixed-point theorem by Joseph Miller by which parametric oracle computations defeat Cantor’s diagonalization. Further investigations of the new topos reveal a strange world in which the Hilbert cube is countable, the Cauchy reals are uncoutable, every function is continuous, there is a countable cover of [0,1] by open intervals without a finite subcover, but every countable cover of [0,1] by open intervals with rational endpoints has a finite subcover. Joint work with James Hanson.
  • 15:30 Break
  • 15.45: Karl Palmskog -- Equivocation-based theory and tools for verifying distributed systems with faults in Coq
    Reasoning formally about distributed systems subject to faults is difficult, and may require establishing tolerance to component misbehavior ranging from simple crashes to unrestricted Byzantine adversarial actions. In this talk, I will present the theory of Validating Labeled State transition and Message production systems (VLSM), a recent proposal for describing and proving properties of such distributed systems. Rather than Byzantine faulty behavior, VLSM theory focuses on equivocation, where components claim different beliefs about the state of the protocol to different parts of the system in order to steer the protocol-abiding components into making inconsistent decisions. An equivocating component behaves as running multiple copies of a protocol, and messages received from equivocating components appear to be valid messages. I will describe how we formalized VLSM theory in Coq, and how this formalization can be used as a framework for verification of distributed protocols. To demonstrate the framework's functionality and expressiveness, I will use some simple examples, starting from VLSMs performing arithmetic operations and leading up to a formalization of the ELMO family of message validating protocols emerging from the Ethereum blockchain community. A key result connects the framework to Byzantine behavior, which states that the effect that Byzantine components with unrestricted faults can have on honest, well-behaving components is no different than the effect equivocating components can have on non-equivocating components. I will highlight how this result can be instantiated for ELMO, intuitively establishing that equivocation analysis of ELMO also provides Byzantine fault tolerance analysis. Joint work with Vlad Zamfir, Denisa Diaconescu, Wojciech Kołowski, Brandon Moore, Traian Florin Șerbănuță, and many others at Runtime Verification, Inc.
  • 16:45 Break
  • 17.00: Vincent Rahli --Realizing Continuity Principles Using Effectful Computations
    The principle of continuity is a seminal property that holds for a number of intuitionistic theories such as System T, MLTT, and BTT, and is inconsistent with classical logic. Most commonly, continuity states that a function from the Baire space to numbers, only needs approximations of the points in the Baire space to compute. Generally, continuity principles have been justified using semantical arguments, but it is known that the modulus of continuity of functions can be computed using effectful computations such as exceptions or references. In this talk, we will present a class of intuitionistic theories that feature stateful computations, such as reference cells, and will explain how to extend these theories with continuity axioms such that they have some computational content in the sense that the modulus of continuity of a functional on the Baire space is directly computed using the stateful computations enabled in the theory. We will further show how this result can be applied to derive more general'' continuity principle, and in particular an inductive'' continuity principle that implies the former notion as well as a uniform variant. If time permits we will also discuss the impact of having effectful computations on other standard axioms such as the Law of Excluded middle and Markov's Principle.
  • 18.00 End of the afternoon session.


Contact

Assia Mahboubi and Pierre-Marie Pédrot