A correspondence between type checking via reduction and type checking via evaluation

DOI10.1016/J.IPL.2011.10.008zbMATH Open1233.68157OpenAlexW2061740608MaRDI QIDQ763480FDOQ763480

Authors: Ilya Sergey, Dave Clarke 

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

Recommendations

• Possible forms of evaluation or reduction in Martin-Löf type theory
• ON THE REDUCTION OF TYPE THEORY
• A type reduction from proof-conditional to dynamic semantics
• Typed Lambda Calculi and Applications
• Reducibility of types in typed lambda calculus. Comment on a paper by Richard Statman
• An extensible equality checking algorithm for dependent type theories
• Publication:4490749
• scientific article; zbMATH DE number 1722651
• Reductions, intersection types, and explicit substitutions
• A semantics for type checking

zbMATH Keywords

functional programmingformal semanticscontinuation-passing styledefunctionalizationcompositional evaluatorsrefunctionalizationtype checkers

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Cites Work

• Types and programing languages
• From reduction-based to reduction-free normalization
• Refunctionalization at work
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
• A Rational Deconstruction of Landin's SECD Machine with the J Operator
• Semantics engineering with PLT Redex
• A Rewriting Semantics for Type Inference
• A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
• A concrete framework for environment machines

Cited In (2)

• Mechanisms for improved covariant type-checking
• Proofs, Upside Down

Uses Software

• Scala

This page was built for publication: A correspondence between type checking via reduction and type checking via evaluation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q763480)