A Relational Realizability Model for Higher-Order Stateful ADTs
作者： Lars Birkedal , Kristian Støvring , Jacob Thamsborg
DOI: 10.1016/J.JLAP.2012.03.004
关键词:
摘要: We present a realizability model for reasoning about contextual equivalence of higher-order programs with impredicative polymorphism, recursive types, and mutable state. The combines the virtues two recent earlier models: (1) Ahmed, Dreyer, Rossberg’s step-indexed logical relations model, which was designed to facilitate proofs representation independence \state-dependent" ADTs (2) Birkedal, Stvring, Thamsborg’s abstract without tedious step-index arithmetic. resulting can be used give ADTs.
elsevier.com
core.ac.uk 
sci-hub.se 参考文章(32)
Lars Birkedal, Kristian Støvring, Jacob Thamsborg, Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types joint european conferences on theory and practice of software. pp. 456- 470 ,(2009) , 10.1007/978-3-642-00596-1_32
John C. Reynolds, Types, Abstraction and Parametric Polymorphism. ifip congress. pp. 513- 523 ,(1983)
Erik de Vink, Jaco de Bakker, Control Flow Semantics ,(1996)
Nick Benton, Benjamin Leperchey, Relational reasoning in a nominal semantics for storage international conference on typed lambda calculi and applications. ,vol. 3461, pp. 86- 101 ,(2005) , 10.1007/11417170_8
Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction ,(1993)
Gordon Plotkin, John Power, Notions of Computation Determine Monads foundations of software science and computation structure. pp. 342- 356 ,(2002) , 10.1007/3-540-45931-6_24
Benjamin C. Pierce, Types and Programming Languages ,(2002)
Nina Bohr, Lars Birkedal, Relational Reasoning for Recursive Types and References Programming Languages and Systems. pp. 79- 96 ,(2006) , 10.1007/11924661_5
I. D. B. Stark, A. M. Pitts, Operational reasoning for functions with local state Higher order operational techniques in semantics. pp. 227- 274 ,(1999)
Sam Staton, Completeness for algebraic theories of local state foundations of software science and computation structure. pp. 48- 63 ,(2010) , 10.1007/978-3-642-12032-9_5