Dependent types ensure partial correctness of theorem provers

Andrew W. Appel, Amy P. Felty

Research output: Contribution to journalArticlepeer-review

14 Scopus citations

Abstract

Static type systems in programming languages allow many errors to be detected at compile time that wouldn't be detected until runtime otherwise. Dependent types are more expressive than the type systems in most programming languages, so languages that have them should allow programmers to detect more errors earlier. In this paper, using the Twelf system, we show that dependent types in the logic programming setting can be used to ensure partial correctness of programs which implement theorem provers, and thus avoid runtime errors in proof search and proof construction. We present two examples: a tactic-style interactive theorem prover and a union-find decision procedure.

Original languageEnglish (US)
Pages (from-to)3-19
Number of pages17
JournalJournal of Functional Programming
Volume14
Issue number1
DOIs
StatePublished - Jan 2004

All Science Journal Classification (ASJC) codes

  • Software

Fingerprint Dive into the research topics of 'Dependent types ensure partial correctness of theorem provers'. Together they form a unique fingerprint.

Cite this