loading...
Modified Realizability Interpretation of Classical Linear Logic
Wroclaw, Poland July 10-July 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2007.3222nd Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Paulo Oliva, Queen Mary, University of London, UK
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.
Citation:
Paulo Oliva, "Modified Realizability Interpretation of Classical Linear Logic," lics, pp.431-442, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.