Mtac: A monad for typed tactic programming in Coq

DOI10.1017/S0956796815000118zbMath1420.68189MaRDI QIDQ5371944

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

Publication date: 23 October 2017

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

Mathematics Subject Classification ID

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

Uses Software

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