DocumentCode :
3300003
Title :
Continuation models are universal for λμ-calculus
Author :
Hofmann, Martin ; Streicher, Thomas
Author_Institution :
Tech. Hochschule Darmstadt, Germany
fYear :
1997
fDate :
29 Jun-2 Jul 1997
Firstpage :
387
Lastpage :
395
Abstract :
We show that a certain simple call-by-name continuation semantics of Parigot´s λμ-calculus (1992) is complete. More precisely, for every λμ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λμ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λμ-category in the sense of is isomorphic to a continuation model derived from a cartesian-closed category of continuations
Keywords :
computation theory; formal logic; functional programming; lambda calculus; abstract continuations; cartesian closed category; cartesian-closed category; continuation model; continuation models; continuation-style interpretation; lambdamu-calculus; simple call-by-name continuation semantics; Arithmetic; Artificial intelligence; Calculus; Concrete; Equations; Functional programming; Lab-on-a-chip; Logic programming; Prototypes;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 1997. LICS '97. Proceedings., 12th Annual IEEE Symposium on
Conference_Location :
Warsaw
ISSN :
1043-6871
Print_ISBN :
0-8186-7925-5
Type :
conf
DOI :
10.1109/LICS.1997.614964
Filename :
614964
Link To Document :
بازگشت