Embedding display calculi into logical frameworks: Comparing twelf and isabelle

Jeremy E. Dawson; Rajeev Goré

doi:10.1016/S1571-0661(04)80880-6

Embedding display calculi into logical frameworks: Comparing twelf and isabelle

Jeremy E. Dawson, Rajeev Goré

Research output: Contribution to journal › Conference article › peer-review

6 Citations (Scopus)

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.

Original language	English
Pages (from-to)	89-103
Number of pages	15
Journal	Electronic Notes in Theoretical Computer Science
Volume	42
DOIs	https://doi.org/10.1016/S1571-0661(04)80880-6
Publication status	Published - Jan 2001
Event	Computing: The Australasian Theory Symposium (CATS 2001) - Gold Coast, Australia Duration: 29 Jan 2001 → 30 Jan 2001

Access to Document

10.1016/S1571-0661(04)80880-6

Cite this

@article{5eea7f578b8241808e1851cec3fd3fa4,

title = "Embedding display calculi into logical frameworks: Comparing twelf and isabelle",

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.",

author = "Dawson, {Jeremy E.} and Rajeev Gor{\'e}",

year = "2001",

month = jan,

doi = "10.1016/S1571-0661(04)80880-6",

language = "English",

volume = "42",

pages = "89--103",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

note = "Computing: The Australasian Theory Symposium (CATS 2001) ; Conference date: 29-01-2001 Through 30-01-2001",

}

TY - JOUR

T1 - Embedding display calculi into logical frameworks

T2 - Computing: The Australasian Theory Symposium (CATS 2001)

AU - Dawson, Jeremy E.

AU - Goré, Rajeev

PY - 2001/1

Y1 - 2001/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=18944372684&partnerID=8YFLogxK

U2 - 10.1016/S1571-0661(04)80880-6

DO - 10.1016/S1571-0661(04)80880-6

M3 - Conference article

AN - SCOPUS:18944372684

SN - 1571-0661

VL - 42

SP - 89

EP - 103

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

Y2 - 29 January 2001 through 30 January 2001

ER -

Embedding display calculi into logical frameworks: Comparing twelf and isabelle

Abstract

Access to Document

Other files and links

Fingerprint

Cite this