Towards logical frameworks in the heterogeneous tool set Hets

DOI10.1007/978-3-642-28412-0_10MaRDI QIDQ2890328zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Mihai Codescu, Fulya Horozal, Michael Kohlhase, Till Mossakowski, Florian Rabe, Kristina Sojakova

Publication date 8 June 2012

Published in Recent Trends in Algebraic Development Techniques (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28412-0_10

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Abstract data types; algebraic specification (68Q65) Logic in artificial intelligence (68T27)

Recommendations

• A logical framework combining model and proof theory
• Logic representation in LF
• scientific article; zbMATH DE number 4180831
• scientific article; zbMATH DE number 2110615
• A proof theoretic interpretation of model theoretic hiding

Cites work

• A formulation of the simple theory of types
• A framework for defining logics
• A logical framework combining model and proof theory
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• CASL: the Common Algebraic Specification Language.
• Development graphs -- proof management for structured specifications
• Encoding modal logics in logical frameworks
• Formalising foundations of mathematics
• scientific article; zbMATH DE number 1617292 (Why is no real title available?)
• scientific article; zbMATH DE number 1231537 (Why is no real title available?)
• scientific article; zbMATH DE number 753781 (Why is no real title available?)
• Institution-independent model theory
• Institutions: abstract model theory for specification and programming
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Representing model theory in a type-theoretical logical framework
• Structural cut elimination. I: Intuitionistic and classical logic
• Structured formal development in Isabelle
• Structured theory presentations and logic representations

Cited in

(11)

• Structure-preserving diagram operators
• Compiling logics
• A proof theoretic interpretation of model theoretic hiding
• How to identify, translate and combine logics?
• scientific article; zbMATH DE number 4180831 (Why is no real title available?)
• A scalable module system
• Project abstract: logic atlas and integrator (LATIN)
• A Maude environment for CafeOBJ
• The distributed ontology, modeling and specification language -- DOL
• A logical framework combining model and proof theory
• Parchments for CafeOBJ logics

Describes a project that uses

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• CASL
• Mizar
• Maude
• Nuprl
• Twelf
• Hets
• Delphin

This page was built for publication: Towards logical frameworks in the heterogeneous tool set Hets

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