Rencontre, Oct. 17, 2024
La rencontre aura lieu en amphi B, sur le site Monod de l'ENS de Lyon.
La rencontre sera diffusée en ligne, à l'adresse suivante : https://bigbluebutton2.enslyon.fr/b/danxnb2klecy le code d'accès est 678064 à l'envers, et il faut penser à autoriser les popups.
Programme
 10:30 – 12:00

Dominik Kirst (IRIF  Université Paris Cité)
Markov's principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ1propositions (i.e. existential quantification over a decidable predicate on N) are stable under double negation. However, there are various nonequivalent definitions of decidable predicates and thus Σ1propositions in constructive foundations, leading to nonequivalent Markov's principles. While this fact is wellreported in the literature, it is often overlooked, leading to wrong claims in standard references and published papers.
In this talk, I will illustrate the status of three natural variants of MP in MartinLöf's constructive type theory (MLTT), by first giving respective equivalence proofs to different formulations of Post's theorem, stability of termination of computations, completeness of various proof systems w.r.t. some modeltheoretic semantics for Σ1theories, and finiteness principles for both extended natural numbers and trees. Afterwards, I describe how these three variants of MP can be separated using effectful models of MLTT, adapting Kreisel’s original proof strategy using free choice sequences to Cohen and Rahli’s framework of stateful type theories.
 13:45 – 14:45

Jonas Frey (LIPN, Université Sorbonne ParisNord)Invited talk: The shape of contexts
Contexts x_1:A_1,...,x_n:A_n in simple type theory can be viewed as “flat”, since the variable declarations don’t depend on each other and can be permuted.
In dependent type theory, the general form of contexts is (x_1:A_1, x_2:A_2(x_1), ...,x_n:A_n(x_1,...,x_{n1})) with a linear dependency chain between the variable declarations: However, the specific contexts occuring in practice are not always totally ordered. For example, in the context (x y:O, f:A(x,y)) the first two variables are not interdependent.
So maybe we should allow finite posets as shapes of contexts? It turns out to be better to use an even more general class of structures: finite direct categories, i.e. finite categories which have no nontrivial isomorphisms and endomorphisms.
FDCs were introduced by Makkai [1] as part of his notion of “First order logic with dependent sorts”, but the perspective on FDCs proposed in this talk is somewhat different since FDCs are not used to represent dependency structures of theories, but of contexts.
In the talk I will explain why FDCs seem to provide a good abstract notion of “shape” for contexts, that the category of FDCs and discrete fibrations forms a coclan, and how to derive a notion of dependent algebraic theory from these ideas which is very close to Chaitanya Leena Subramaniam’s “dependently typed theories”.
[1] https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf
 15:15 – 16:15

PierreMarie Pédrot (Galinette, INRIA)Invited talk: Upon This Quote I Will Build My Church Thesis
The internal Church thesis (CT) is a logical principle stating that any function f : N → N is computed by a concrete program in some Turingcomplete language. CT has been widely used in constructive mathematics, most specifically in the Russian tradition. On the other side of the iron curtain, MartinLoef Type Theory (MLTT) was designed as the modern embodiment of Bishopstyle neutral mathematics. It should come as a surprise that the natural typetheoretic equivalent of CT was conjectured to be inconsistent with MLTT. In this talk, we will prove that this conjecture is false, by introducing “MLTT”, a consistent extension of MLTT with quoting primitives that implements CT in a computational way.