A correspondence between type checking via reduction and type checking via evaluation
From MaRDI portal
Publication:763480
DOI10.1016/j.ipl.2011.10.008zbMath1233.68157OpenAlexW2061740608MaRDI 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 semanticsfunctional programmingcontinuation-passing styledefunctionalizationcompositional evaluatorsrefunctionalizationtype checkers
Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
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
This page was built for publication: A correspondence between type checking via reduction and type checking via evaluation