Séminaire, 5 février 2015

Programme

10:30 – 12:00

Jörg Endrullis (Vrije Universiteit Amsterdam)

Invited talk: Clocked lambda-calculus

(This talk will be given in room B1, fourth floor)

14:00 – 15:00

Anupam Das (LIP, ENS Lyon)

Invited talk: Theories of bounded arithmetic for deep inference proof systems

We give uniform versions of propositional logic deep inference systems in the setting of 'bounded arithmetic', relating the size of propositional proofs to forms of proof-theoretic strength in fragments of arithmetic.

This continues the recent program of studying the complexity of deep inference proofs by bringing it in line with the standards of mainstream proof complexity. It is also inspired by previous work where proofs of the propositional pigeonhole principle in the minimal deep inference system, KS, were constructed using rather abstract uniform templates, suggesting the need for such an approach.

To minimise prerequisites we work in the setting of monotone proofs represented as rewriting derivations, isolating fragments of so-called 'analytic' deep inference. For the same reason we construct our arithmetic theories by adapting the well studied IDelta_0 of Parikh, Paris, Wilkie and others, although similar theories could be designed using the more modern second-order setting of Zambella, Cook and Nguyen.

Along the way we require a blend of tools from bounded arithmetic (correspondence with propositional proofs), deep inference (efficient normalization of propositional translations), and descriptive complexity (taming the closure functions of least fixed point operators used to simulate deep inference).

15:30 – 16:30

Andrew Polonski (PPS-LIPN)

Invited talk: Toward extensional type theory with decidable type-checking

We report our work on a new treatment of equality in dependent type theory.

Large-scale formalization of mathematics in type theory is greatly impededed by the intensional character of type-theoretic equality. For a variable n:Nat, the terms n+1 and 1+n are equal but not convertible. Consequently, if B(n) is a dependent type over N (eg. R^n), then B(n+1) and B(1+n) are isomorphic but not equal; thus there is no automatic way to transfer properties from one type to another. The terms S=(\n.n+1) and S'=(\n.1+n) of type Nat->Nat are not even equal propositionally, thus there is no explicit isomorphism between types B(S) and B(S') when B(f) is a type dependent over Nat->Nat. Martin-Lof defined extensional type theory by reflecting the equality proofs (terms of the identity type) into the conversion relation. Unfortunately, this renders type-checking and proof-checking undecidable, undermining a major motivation for working in type theory.

Voevodsky recently proposed the Univalence Axiom which solves the problem of extensionality, but, without a computational justification, leads to the failure of canonicity, another crucial metatheoretic property. Coquand et al have recently provided this missing piece by building a model of univalence in constructive metatheory.

We propose an alternative, syntax-based approach to extensionality. In this approach, the equality type is initially defined externally, as a logical relation on the term model of type theory, which in turn is defined by induction on type structure. The relation is then reflected into the language by extending the syntax. This results in a 1-dimensional theory; in order to have equality as a type constructor that can be iterated (so that we can write p,q : Eq(A,a,b), pi : Eq(Eq(A,a,b),p,q), etc.), the reflection operation must itself be internalized. We show how this can be done in a consistent way, and verify some basic properties of the resulting system.