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.

• Type: Journal
• Year: 2012
• Where: LICS
• Authors: Naohiko Hoshino
• Keywords: Automated Reasoning, Categorical Abstract Machine, Lambda Calculi, Lambda Calculus, LICS 2012