Embedding Display Calculi into Logical Frameworks: Comparing Twelf and Isabelle
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]
|Collections||ANU Research Publications|
|Source:||CATS: Computing, The Australian Theory Symposium|
|01_Dawson_Embedding_Display_Calculi_into_2001.pdf||198.28 kB||Adobe PDF||Request a copy|
|02_Dawson_Embedding_Display_Calculi_into_2001.pdf||148.78 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.