Logic & Programming

Danko Ilik's research blog
<– home page

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.

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

Title: High-school sequent calculus and an intuitionistic formula hierarchy preserving identity of proofs

http://ls.informatik.uni-tuebingen.de/GPT/

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

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

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