Paper: Modified Realizability Interpretation of Classical Linear Logic (at LICS 2007)

Authors: Paulo Oliva

Abstract

This paper presents a modified realizability interpretation of classical linear logic. The interpretation is based on work of de Paiva (1989), Blass (1995), and Shirahata (2006) on categorical models of classical linear logic using G¨odel’s Dialectica interpretation. Whereas the Dialectica categories provide models of linear logic, our interpretation is presented as an endo-interpretation of proofs, which does not leave the realm of classical linear logic. The advantage is that we obtain stronger versions of the disjunction and existence properties, and new conservation results for certain choice principles. Of particular interest is the simple branching quantifier used in order to obtain a completeness result for the modified realizability interpretation.

BibTeX

  @InProceedings{Oliva-ModifiedRealizabili,
    author = 	 {Paulo Oliva},
    title = 	 {Modified Realizability Interpretation of Classical Linear Logic},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {431--440},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }