Mtac: A monad for typed tactic programming in Coq

DOI10.1017/S0956796815000118zbMath1420.68189OpenAlexW2277214925MaRDI QIDQ5371944

Neelakantan R. Krishnaswami, Beta Ziliani, Viktor Vafeiadis, Derek R. Dreyer, Aleksandar Nanevski

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796815000118

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ The \textsc{MetaCoq} project ⋮ Harpoon: mechanizing metatheory interactively

Uses Software

• Coq
• CompCertTSO
• Paco
• Ynot
• Mtac
• Rtac
• VeriML
• seL4
• Delphin

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A compact kernel for the calculus of inductive constructions
• Inductive types and type constraints in the second-order lambda calculus
• Compositional Computational Reflection
• Synthesis of Distributed Mobile Programs Using Monadic Types in Coq
• The power of parameterization in coinductive proof
• Static and user-extensible proof checking
• Programming with binders and indexed data-types
• Meta-programming with names and necessity
• A compiled implementation of strong reduction
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• First-Class Type Classes
• Hoare type theory, polymorphism and separation
• Subset Coercions in Coq
• A framework for defining logics
• VeriML
• Ynot
• Typed syntactic meta-programming
• Mtac
• Structuring the verification of heap-manipulating programs
• Contextual modal type theory
• Mathematical Knowledge Management
• Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation
• A Machine-Checked Proof of the Odd Order Theorem
• Adjustable References
• CompCertTSO
• How to make ad hoc proof automation less ad hoc
• Typed Lambda Calculi and Applications
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

This page was built for publication: Mtac: A monad for typed tactic programming in Coq