Towards logical frameworks in the heterogeneous tool set Hets

DOI10.1007/978-3-642-28412-0_10zbMATH Open1278.68286DBLPconf/wadt/CodescuHKMRS10OpenAlexW111349018WikidataQ57389377 ScholiaQ57389377MaRDI QIDQ2890328FDOQ2890328

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

Recommendations

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (10)

• A logical framework combining model and proof theory
• A scalable module system
• Title not available (Why is that?)
• Parchments for CafeOBJ logics
• Structure-preserving diagram operators
• The Distributed Ontology, Modeling and Specification Language – DOL
• A proof theoretic interpretation of model theoretic hiding
• Compiling logics
• Project abstract: logic atlas and integrator (LATIN)
• A Maude environment for CafeOBJ

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)