Publikation
Towards Logical Frameworks in the Heterogeneous Tool Set Hets
Mihai Codescu; Fulya Horozal; Michael Kohlhase; Till Mossakowski; Florian Rabe; Kristina Sojakova
In: Hans-Jörg Kreowski; Till Mossakowski (Hrsg.). Recent Trends in Algebraic Development Techniques. International Workshop on Algebraic Development Techniques (WADT-10), 20th, July 1-4, Schloss Etelsen, Germany, Lecture Notes in Computer Science (LNCS), Vol. 7137, Springer, 2012.
Zusammenfassung
LF is a meta-logical framework that has become a standard
tool for representing logics and studying their properties. Its focus is
proof theoretic, employing the Curry-Howard isomorphism: propositions
are represented as types, and proofs as terms.
Hets is an integration tool for logics, logic translations and provers, with
a model theoretic focus, based on the meta-framework of institutions, a
formalisation of the notion of logical system.
In this work, we combine these two worlds. The benefit for LF is that
logics represented in LF can be (via Hets) easily connected to various
interactive and automated theorem provers, model finders, model checkers,
and conservativity checkers - thus providing much more efficient proof
support than mere proof checking as is done by systems like Twelf. The
benefit for Hets is that (via LF) logics become represented formally, and
hence trustworthiness of the implementation of logics is increased, and
correctness of logic translations can be mechanically verified. Moreover,
since logics and logic translations are now represented declaratively, the
effort of adding new logics or translations to Hets is greatly reduced.
This work is part of a larger effort of building an atlas of logics and
translations used in computer science and mathematics.