Abstract: Logical incarnations of type isomorphism include the notions of constructive cardinality of sets and strong intuitionistic equivalence of formulas. These are challenging to study in simultaneous presence of functions (exponentials) and sums (disjoint unions, disjunction). In this talk, I will present a quasi-normal form of types that arises from the decomposition of binary exponentiation into the unary exponentiation and logarithm. This normal form can be applied for disentangling the equational theory (beta-eta) of the lambda calculus with sums. By an extension of the normal form from simple types (propositional logic) to quantifiers, one can also retrieve an “arithmetical” hierarchy for intuitionistic first order logic. Finally, this suggests a sequent calculus for intuitionistic logic that uses the notation of exponential polynomials and removes the need for most of the invertible proof rules of usual sequent calculi.
In presence of sum types, the lambda calculus does not enjoy uniqueness of eta-long normal forms. The canonicity
problem also appears for proof trees of intuitionistic logic. In
this talk, I will show how the problem becomes easier if, before
choosing a canonical representative from a class of
beta-eta-equal terms, one coerces the term into the exp-log
normal form of its type. This type normal form arises from the
one for exponential polynomials.
On March 9, I am giving a talk at the Gallium seminar. Abstract: In this talk, I will present some recent results from Proof
Theory that might also be interesting to Programming Languages Theory.
First, I will present work on isomorphisms of types in presence of sums,
as well as the implications for canonicity of eta-long normal forms of
lambda calculus with sums. Second, I will show how one can use a
normalization-by-evaluation proof (written in CPS style) to compile away
control operators from System T; this could be used as a compiler
technique for a side-effect-free fragment of a program.
On January 21st, I am giving a talk at GdT Théorie des types et réalisabilité. Abstract: The traditional method to extract programs from proofs of classical Analysis (Peano Arithmetic + Axiom of Choice) is to use an extension of Gödel's System T with bar recursion. An alternative method is to use an approach based on computational side-effects (control operators, quote/clock instructions) like in the works of Krivine or Herbelin. By classic results of Kreisel and Schwichtenberg, for the fragment of Analysis that makes sense computationally, the Π₂-fragment, we know that bar recursion is essentially primitive recursive — leaving open the question of how to actually avoid using it. In this talk, I will present some recent work (http://arxiv.org/abs/1301.5089) showing how realizers of System T can be extracted directly from proofs of the Σ₂-fragment of classical Analysis. Control operators are essential, but only at the meta-theoretical level: control operators can be compiled away from System T, at any simple type.
I am giving a distilled tutorial during the conference PPDP 2014. The topic is writing proofs in continuation passing style, with the xase study of normalization-by-evaluation for Gödel's System T extended with delimited control. Tutorial web page is up.