Formath
Lundi 16 décembre 2024, 14 heures, 3052 et en visio
Meven Lennon-Bertrand (Cambridge) MetaCoq tutorial
If you want to play around live, I recommend installing the coq-metacoq-template opam package beforehand, and to check that you can step through this file: https://github.com/MetaCoq/tutorials/blob/main/popl24/exercises/MetaCoqPrelude.v
This session of Formath will be longer than usual as the tutorial will last about 1h45/2h.
Formath
Lundi 2 décembre 2024, 14 heures, 3052 (+visio)
Loïc Pujet (Stockholm University) Cellular Methods in Homotopy Type Theory
In this talk, we will look at the classical theory of CW complexes and investigate which parts can be reproduced constructively in type theory. In particular, we will focus on the cellular approximation theorem, the Hurewicz theorem, and the use of cellular homology to compute homology groups.
This is joint work with Axel Ljungström and Anders Mörtberg.
Le séminaire sera accessible en visio à https://orsay.bbb.cnrs.fr/b/sau-vga-oqv-ekl
Formath
Lundi 25 novembre 2024, 15 heures 30, 3052
Alexandre Moine (Courant Institute, New York University) Reaching for Unreachability Properties in Separation Logic
In the first part, I will present my PhD thesis work: an Iris-fueled Separation Logic with space credits, allowing for the verification of heap space bounds in the presence of concurrency and garbage collection. Crucially, this logic tracks the reachability of heap objects in a modular way, and allows for recovering space credits when the user proves an object unreachable.
In the second part, I will present another line of work about disentanglement. Disentanglement is a property of parallel programs asserting that a location allocated by a task must remain unreachable by concurrently executing tasks. Making use of disentanglement, the MPL (MaPLe) compiler for parallel ML equips programs with a blazingly fast, task-local, garbage collector. I will present DisLog, an Iris-fueled Separation Logic for verifying disentanglement, and present ongoing work on TypeDis, a type system for automatically verifying disentanglement.
Attention à l'horaire inhabitutel! Séance conjointe avec le GT Programmation
Formath
Lundi 14 octobre 2024, 14 heures, 3063
Emilio Gallego Arias (Picube, IRIF) jsCoq 2.0: Towards interactive formal mathematical documents
jsCoq began in 2015 as an experiment to test the js_of_ocaml compiler, later evolving to offer an install-free distribution of math-comp proofs in a convenient presentation format.
The combination of a) an install-free Coq setup, b) full-featured package manager with many contributions available, and c) a literate programming format made jsCoq quite popular within the Coq teaching community.
However, the first jsCoq implementation had several limitations in terms of usability, document expressiveness, and constraints inherent to Coq’s standard document manager, the STM.
Work began in 2016 to replace the STM with a model better suited for jsCoq's rich document model and usability needs, culminating in 2022 with Flèche, a new document manager for Coq specifically designed to accommodate jsCoq use cases.
In this talk, we will introduce jsCoq 2, a major update to the jsCoq based on Flèche and the coq-lsp language server.
jsCoq 2 offers a continuous interaction model better suited for teaching and directly supports rich, jsCoq-style documents. This update addresses many technical challenges and enables users to develop courses and interactive documents entirely in the browser, using different editors, including rich WYSIWYG ones.
We will discuss the context and design requirements behind jsCoq and Flèche, providing a detailed overview of jsCoq 2's main features, novelties, and future roadmap.
jsCoq 2 is joint work with Shachar Itzhaky (Technion - Israel Institute of Technology).
Formath
Lundi 7 octobre 2024, 14 heures, 3052
Nadine Karsten (TU Berlin, Chair: Models and Theory of Distributed Systems) ProofBuddy - The way to teach proofs structures?
However, proof assistants are not made for beginners. Moreover, learning formal and mathematical language at the same time is often overwhelming. We develop the web interface ProofBuddy based on the proof assistant Isabelle as a tool that (also) targets for beginners. We chose Isabelle, because we assume that the proximity of its Isar language to natural/mathematical language supports the learning process. Pedagogically, we experiment with a setting in which students constantly switch between pen-and-paper-proofs and their formal counterparts. ProofBuddy is designed to support this back-and-forth approach.
In the talk, I report on the architecture and the user interface of ProofBuddy, give a short introduction to Isar within ProofBuddy and present our pedagogical approach.
Formath
Lundi 30 septembre 2024, 14 heures, 3052
Dominik Kirst (Picube, IRIF) Mechanised Constructive Reverse Mathematics: The Examples of Completeness, Löwenheim-Skolem Theorems, and Post's Problem
In this talk, I will give an overview of some ongoing projects concerning Gödel's completeness theorem for first-order logic, the related Löwenheim-Skolem theorems, as well as Post's problem concerning the existence of a semi-decidable yet undecidable Turing degree strictly below the halting problem. Especially the latter exploits a synthetic approach to computability theory available in any constructive foundation, where the reference to an explicit model of computation can be disposed of by simply considering every function to be computable.
Formath
Lundi 16 septembre 2024, 14 heures, 3052
Marc Bezem (University of Bergen, Norway) The Max-Atom Problem applied to Universe Polymorphism in Type Theory
In the second half of the talk we propose a type theory with explicit universe polymorphism, featuring level-indexed product types and constraint-indexed product types. In this type theory, loop checking and uniform word problems in the above mentioned lattices play a crucial role.
Efficiency and complexity issues will briefly be addressed throughout the talk. The research presented here is joint work with many people: Nieuwenhuis, Rodríguez-Carbonell, Coquand, Dybjer, Escardó.
Le séminaire sera accessible en visio à https://orsay.bbb.cnrs.fr/b/sau-vga-oqv-ekl
Formath
Lundi 10 juin 2024, 14 heures, 3052 and bbb Link
Sarah Reboullet (Université Paris Cité, IRIF & INRIA Picube) Fixing Internal Parametricity and Its Presheaf Model
Formath
Lundi 27 mai 2024, 14 heures, 3052 and Zoom Link
Laetitia Teodorescu (IRIF, Université Paris Cité & INRIA FLOWERS & Picube) Autotelic machine learning for programming and mathematics
Formath
Lundi 29 avril 2024, 14 heures, 3052 and bbb Link
Hugo Herbelin (Picube) Où se cache le calcul dans les topos élémentaires ?
En tout cas, on commencera par voir le classificateur de sous-objet comme un hProp imprédicatif, par isoler le rôle de l'extensionnalité des propositions (= univalence pour hProp) dans la correspondance entre représentations fibrées et indexées des prédicats dans les topos, et par comprendre comment la somme disjointe peut se simuler en combinant le pouvoir de décision de la définition imprédicative de la disjonction avec le pouvoir de représentation des types par des parties singleton.
Formath
Mardi 26 mars 2024, 14 heures, 1020 and Renater
Lasse Blaauwbroek A machine learning platform for proof synthesis in Coq
In this talk, I will give a general tutorial on Tactician. We start with a usage demonstration from an end-user perspective. Then we'll take a look at Tactician's internal architecture. There are several data formats for machine learning, including a novel graph-based representation of the Calculus of Existential Inductive Constructions, where every node in the graph represents a unique term modulo alpha-equivalence. This data is made available both as an offline dataset and through interaction with Coq using a rich remote procedure calling (RPC) protocol. We'll see how we can easily implement our own external solving agent in Python.
Formath
Lundi 18 mars 2024, 14 heures, Grenoble
Gdr Ifm Journées nationales du GDR (pas d'exposé)
Formath
Lundi 11 mars 2024, 14 heures, 3052
Gabriel Scherer Random generation of well-typed terms: a constraint-based approach
Most existing generators integrate a large part of the implementation of a type-checker, “inverted” to assist in top-down random term generation by efficiently discarding choices that result in ill-typed programs. Scaling this approach to a full language would result in implementing two sophisticated type-checkers, once in the compiler and once in the program generator. This is one type-checker too many!
In this talk I will present preliminary work on reusing the constraint-based type inference approach [The Essence of ML-based type inference, Pottier and Rémy, 2004] to write a single type-checker that can be used for both purposes: to check types of user-provided programs, and to efficiently guide a random program generator. This only requires a fairly simple modification to constraint generators: parametrizing them over a search monad.
(Relevant previous work is [Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System, Fetscher, Claessen, Pałka, Hughes, Findler]. They start from Redex, a Racket DSL to implement simple type systems, and derive a random program generator. The limitation of this approach is that Redex only works with fairly simple type system, in particular we do not expect it to scale to ML-style type inference with polymorphism, which is the part that hand-crafted generators also struggle on. Our work builds on top of constraint-solving approaches that are known to scale well to ML-style polymorphic; but it is preliminary and we have only implemented support for the simply-typed lambda-calculus for now.)
Formath
Lundi 4 mars 2024, 14 heures, 3052 and bbb Link
Guillaume Baudart Schedule Agnostic Semantics for Reactive Probabilistic Programming
In talk I will present two schedule agnostic semantics for a probabilistic synchronous language. The key idea is to interpret probabilistic expressions as a stream of un-normalized density functions which maps random variable values to a result and positive score. The co-iterative semantics extends the original semantics to interpret mutually recursive equations using a fixpoint operator. The relational semantics directly manipulates streams and is thus a better fit to reason about program equivalence. We use the relational semantics to prove the correctness of a program transformation required to run an optimized inference algorithm for state-space models with constant parameters.
This is joint work with Louis Mandel and Christine Tasson.
Formath
Lundi 26 février 2024, 14 heures, 3052
Julien Narboux (Université de Strasbourg) Formalization of geometry, and automated theorem proving using constraint solving
Formath
Lundi 12 février 2024, 14 heures, 3052 and bbb Link
Esaïe Bauer (IRIF, Université Paris Cité & INRIA Picube) Cut-elimination for the circular modal mu-calculus: linear logic and super exponentials to the rescue
During this talk, I will present a strategy to prove cut-elimination theorem for the modal mu-calculus. This strategy is to prove cut-elimination for a “linear translation” of the modal mu-calculus (that is to define a translation of the statements and proofs of the modal mu-calculus into a linear sequent calculus) and to deduce the desired cut-elimination results as corollaries.
While designing this linear translation, we come up with a sequent calculus exhibiting several modalities (or exponentials). It happens that the literature of linear logic offers tools to manage such calculi, for instance subexponentials by Nigam and Miller and super exponentials which is a work I did with Olivier Laurent.
We actually extend super exponentials with fixed-points and non-wellfounded proofs (of which the linear decomposition of the modal mu-calculus is an instance) and prove a syntactic cut-elimination theorem for these sequent calculi in the framework of non-wellfounded proof theory.
Back to the classical modal mu-calculus, we deduce its cut-elimination theorem from the above results, investigating both non-wellfounded and regular proofs.
This is a joint work with Alexis Saurin.
Formath
Lundi 22 janvier 2024, 14 heures, 3052 and bbb Link
Houda Mouhcine (Inria Saclay) & Micaela Mayero (Université Paris 13, Lipn, Love) Double exposé
Abstract: Formalizing real numbers in a formal proof tool represents a particular challenge. It is not only a question of representing numbers in computers but also of preserving all mathematical properties needed to make proofs. We will review the history of real numbers formalization in different proof assistants and the different ways of formalizing them, before giving an overview of real numbers libraries that exist today in provers. As application, we will finish by presenting real analysis developments in Coq.
2. [Deuxième exposé : Houda] Title: Formal proofs in applied mathematics: Formalization of Tonelli Theorem and Lagrange Finite Elements
Abstract. Numerical analysis, as an essential tool for solving complex mathematical problems through the use of algorithms and numerical approximations, is further fortified in this work by rigorously formalizing Tonelli's Theorem and Lagrange Finite Elements. These basic concepts are defined and validated using formal proof techniques, enhancing their credibility in various mathematical applications. In the field of integration, important results such as Tonelli's Theorem and the Lebesgue Induction Principle are covered. Furthermore, in the field of numerical resolution of partial differential equations, we explore finite elements, covering the general definition of finite elements, and geometric transformations, up to the full definition of simplicial Lagrange finite elements, including the unisolvance property.
Formath
Lundi 8 janvier 2024, 14 heures, 3052 and Galène Link (password: tensor)
Loïc Pujet (University of Stockholm) Choice Principles in Observational Type Theory
Unfortunately, it is difficult to use these quotients without any choice principles to extract information from proof-irrelevant truncations. In this talk, I will discuss the various choice principles one could hope to have in OTT, and I will use ideas from Higher Observational Type Theory to sketch a version of OTT with unique choice.