Dependent types ensure partial correctness of theorem provers

DOI10.1017/S0956796803004921zbMath1083.68017OpenAlexW2000778709MaRDI QIDQ4819651

Andrew W. Appel, Amy P. Felty

Publication date: 27 September 2004

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

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

Mathematics Subject Classification ID

Related Items (4)

Mechanizing metatheory in a logical framework ⋮ Tactics for hierarchical proof ⋮ A Tactic Language for Hiproofs ⋮ Imperative LF Meta-Programming

Uses Software

• Coq
• Twelf

This page was built for publication: Dependent types ensure partial correctness of theorem provers