Towards Certified Meta-Programming with Typed Template-Coq
Authors:
Open Access
- 4 July 2018
- book chapter
- Published by Springer Nature
- p. 20-39
Abstract
No abstract availableKeywords
This publication has 26 references indexed in Scilit:
- Mtac: A monad for typed tactic programming in CoqJournal of Functional Programming, 2015
- Canonicity of Weak ω-groupoid Laws Using Parametricity TheoryElectronic Notes in Theoretical Computer Science, 2014
- Engineering Proof by Reflection in Agda2013
- Typed syntactic meta-programmingACM SIGPLAN Notices, 2013
- Proofs for freeJournal of Functional Programming, 2012
- Extending Coq with Imperative Features and Its Application to SAT VerificationLecture Notes in Computer Science, 2010
- Type Theory Should Eat ItselfElectronic Notes in Theoretical Computer Science, 2009
- Template meta-programming for HaskellACM SIGPLAN Notices, 2002
- Multi-stage programming with explicit annotationsACM SIGPLAN Notices, 1997
- Theorems for free!1989