A correspondence between type checking via reduction and type checking via evaluation
From MaRDI portal
Publication:763480
DOI10.1016/j.ipl.2011.10.008zbMath1233.68157MaRDI QIDQ763480
Publication date: 9 March 2012
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://lirias.kuleuven.be/handle/123456789/320219
formal semantics; functional programming; continuation-passing style; defunctionalization; compositional evaluators; refunctionalization; type checkers
68N18: Functional programming and lambda calculus
68Q55: Semantics in the theory of computing
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Refunctionalization at work
- On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
- A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
- A Rational Deconstruction of Landin's SECD Machine with the J Operator
- From Reduction-Based to Reduction-Free Normalization
- A concrete framework for environment machines
- A Rewriting Semantics for Type Inference