scientific article; zbMATH DE number 7362470

MaRDI QIDQ4995161zbMATH OpenFDO

Authors Andreas Abel, James Chapman

Publication date 23 June 2021

Full work available at URL https://arxiv.org/abs/1406.2059, http://eptcs.web.cse.unsw.edu.au/paper.cgi?MSFP2014.4

Mathematics Subject Classification ID

Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Normalization by evaluation for modal dependent type theory
• Normalization by Evaluation for Typed Weak lambda-Reduction
• scientific article; zbMATH DE number 3933030
• The simple type theory of normalisation by evaluation
• Typed Applicative Structures and Normalization by Evaluation for System F ω
• Foundations of Software Science and Computation Structures
• Expansion postponement for normalising pure type systems
• Quotienting the delay monad by weak bisimilarity
• Quotienting the delay monad by weak bisimilarity
• Monads, partial evaluations, and rewriting

Cited in

(4)

• Turing-Completeness Totally Free
• Guarded recursion in Agda via sized types
• POPLMark reloaded: mechanizing proofs by logical relations
• Flag-based big-step semantics

Describes a project that uses

Uses Software

• Agda

This page was built for publication:

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