Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle
Date
2001
Authors
Dawson, Jeremy
Gore, Rajeev
Journal Title
Journal ISSN
Volume Title
Publisher
Elsevier
Abstract
Logical frameworks are computer systems which allow a user to formalise mathematics using specially designed languages based upon mathematical logic and Church's theory of types. They can be used to derive programs from logical specifications, thereby guaranteeing the correctness of the resulting programs. They can also be used to formalise rigorous proofs about logical systems. We compare several methods of implementing the display (sequent) calculus δRA for relation algebra in the logical frameworks Isabelle and Twelf. We aim for an implementation enabling us to formalise, within the logical framework, proof-theoretic results such as the cut-elimination theorem for δRA, and any associated increase in proof length. We discuss issues arising from this requirement.
Description
Keywords
Keywords: Church's theory; Logical frameworks; Logical specifications; Relation algebras; Boolean algebra; Computer hardware description languages; Computer science; Computer systems; Formal logic; Linear algebra; Mathematical models; Theorem proving; Logic program
Citation
Collections
Source
CATS: Computing, The Australian Theory Symposium
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31