DocumentCode :
3093010
Title :
Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects
Author :
Hoshino, Naohiko
Author_Institution :
Res. Inst. for Math. Sci., Kyoto Univ., Kyoto, Japan
fYear :
2012
fDate :
25-28 June 2012
Firstpage :
385
Lastpage :
394
Abstract :
We propose a mathematical framework for step indexed realizability semantics of a call-by-value polymorphic lambda calculus with recursion, existential types and recursive types. Our framework subsumes step indexed realizability semantics by untyped call-by-value lambda calculi as well as categorical abstract machines. Starting from an extension of Hofstra´s basic combinatorial objects, we construct a step indexed categorical realizability semantics. Our main result is soundness and adequacy of our step indexed realizability semantics. As an application, we show that a small step operational semantics captures the big step operational semantics of the call-by-value polymorphic lambda calculus. We also give a safe implementation of the call-by-value polymorphic lambda calculus into a categorical abstract machine.
Keywords :
finite automata; lambda calculus; programming language semantics; basic combinatorial objects; big step operational semantics; call-by-value language; call-by-value polymorphic lambda calculus; categorical abstract machines; step indexed realizability semantics; untyped call-by-value lambda calculi; Abstracts; Algebra; Calculus; Indexing; Mathematical model; Semantics; Syntactics; Semantics of Programming Languages; denotational semantics; operational semantics;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science (LICS), 2012 27th Annual IEEE Symposium on
Conference_Location :
Dubrovnik
ISSN :
1043-6871
Print_ISBN :
978-1-4673-2263-8
Type :
conf
DOI :
10.1109/LICS.2012.74
Filename :
6280457
Link To Document :
بازگشت