A compiled implementation of normalisation by evaluation
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- A Compiled Implementation of Normalization by Evaluation
- Flyspeck I: Tame Graphs
- Isabelle/HOL. A proof assistant for higher-order logic
- Operational aspects of untyped Normalisation by Evaluation
- Partial Recursive Functions in Higher-Order Logic
- Term rewriting for normalization by evaluation.
Cited in
(10)- Normalization by evaluation and algebraic effects
- scientific article; zbMATH DE number 1757129 (Why is no real title available?)
- Operational aspects of untyped Normalisation by Evaluation
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- Normalisation by evaluation for type theory, in type theory
- Fast, verified computation for HOL ITPs
- Gale-Shapley verified
- A Compiled Implementation of Normalization by Evaluation
- Normalisation by evaluation for dependent types
- scientific article; zbMATH DE number 5353378 (Why is no real title available?)
This page was built for publication: A compiled implementation of normalisation by evaluation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2913943)
