Danko Ilik's research blog
<– home page
http://imft.ftn.uns.ac.rs/math/cms/LAP2015
Title: Computational interpretations of the classical Axiom of Choice
Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net
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
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