Skip navigation
Skip navigation

Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle

Dawson, Jeremy; Gore, Rajeev

Description

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
URI: http://hdl.handle.net/1885/93299
Source: CATS: Computing, The Australian Theory Symposium
DOI: 10.1016/S1571-0661(04)80880-6

Download

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:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator