Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle

MaRDI QIDQ2703745zbMATH OpenFDO

Authors Rajeev Goré, Jeremy E. Dawson

Publication date 8 May 2001

zbMATH Keywords

Church's theory of typesdRA

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• scientific article; zbMATH DE number 1927419
• The Twelf Proof Assistant
• scientific article; zbMATH DE number 1301758
• A new machine-checked proof of strong normalisation for display logic
• Using typed lambda calculus to implement formal systems on a machine

Cited in

(1)

• scientific article; zbMATH DE number 1927419 (Why is no real title available?)

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2703745)