Skip navigation
Skip navigation

Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle

Dawson, Jeremy; Gore, Rajeev


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...[Show more]

CollectionsANU Research Publications
Date published: 2001
Type: Conference paper
Source: CATS: Computing, The Australian Theory Symposium
DOI: 10.1016/S1571-0661(04)80880-6


File Description SizeFormat Image
01_Dawson_Embedding_Display_Calculi_into_2001.pdf198.28 kBAdobe PDF    Request a copy
02_Dawson_Embedding_Display_Calculi_into_2001.pdf148.78 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator