Paper: A computational analysis of Girard's translation and LC (at LICS 1992)

Authors: Chetan R. Murthy

Abstract

J.-Y. Girard's (1992) new translation from classical to constructive logic is explained. A compatible continuation-passing-style (CPS) translation is given and converted to a C-rewriting machine evaluator for control-operator programs and a set of reduction/computation rules sufficient to represent the evaluator. It is found necessary to add one reduction rule to M. Felleisen's (Ph.D. thesis, Indiana Univ., 1987) calculus (evaluation under λ-abstraction). This reduction rule arises from a modified call-by-name CPS-translation. Turning to Girard's new classical logic LC, an intuitionistic term-extraction procedure is provided for it, producing CPS functional programs. Using the syntactic properties of this language, it is possible to give simple proofs for the evidence properties of LC. This work sheds light on the design space of CPS-translations and extends the relation between control-operator languages and classical logic

BibTeX

  @InProceedings{Murthy-Acomputationalanaly,
    author = 	 {Chetan R. Murthy},
    title = 	 {A computational analysis of Girard's translation and LC},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {90--101},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }