Logic & Programming

Title: On the indispensability of bar recursion

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

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.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

Title: Proof Assistants, marriage of Proof Theory and Programming Languages

http://ciit.finki.ukim.mk/

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

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.

http://gallium.inria.fr/seminar.html

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

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.

http://archives.pps.univ-paris-diderot.fr/gdt-types-realisabilite/index.html

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

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.

https://iaddg.net/danko/PPDP-2014-tutorial/

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

My paper on type isomorphisms in the presence of sums was accepted to CSL-LICS 2014.

http://arxiv.org/abs/1401.2567

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

I will be serving on the program committee for the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP) taking place in Canterbury, UK on September 8-10, 2014

http://www.cs.kent.ac.uk/events/2014/ppdp-lopstr-14/

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

The paper “A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators”, coauthored with Keiko Nakata, accepted for publication

http://arxiv.org/abs/1209.2229

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net

I will give a talk on type isomorphisms on the Deducteam seminar at INRIA Paris — av. de Italie, on February 7, 2014, at 10:00.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net