Sciweavers

LICS
2012
IEEE

Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects

11 years 6 months ago
Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects
—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 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 hic lambda calculus into a categorical abstract machine.
Naohiko Hoshino
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Where LICS
Authors Naohiko Hoshino
Comments (0)