Ludwig-Maximilians-Universität München, Institut für Informatik
Technical Report 93-21
- TITLE:
-
Continuation Semantics or Expressing Implication by Negation
- DATE:
-
to be published
- AUTHORS:
- Yves Lafont
<lafont@dmi.ens.fr>
- Laboratoire d'Informatique
- CNRS - Ecole Normale superieure
- Paris
- Bernhard Reus
<reus@informatik.uni-muenchen.de>
- Thomas Streicher
<streicher@informatik.uni-muenchen.de>
- Institut für Informatik
- Universität München
- Leopoldstr. 11B
- D-80802 München (Germany)
- KEYWORDS:
-
continuations,
continuation passing translation,
proof terms for and,not-fragment of intuitionistic logic, PCF
- ABSTRACT:
-
Starting from the ideas of J.Y. Girard on making classical logic constructive,
we isolate a fragment of intuitionistic logic with negation instead of
implication, and we investigate the corresponding programming paradigm.
In particular, we get a nice continuation passing style translation of
lambda calculus, from which we derive a semantics of non functional features
in functional programming, such as inputs/outputs and Felleisen's C operator.
Bei Problemen, Vorschlägen schicken Sie bitte eine eMail an
wwwmaster@informatik.uni-muenchen.de .
Robert Stabl, 18.01.1994