A Proof Theoretic Interpretation of Model Theoretic Hiding

DOI10.1007/978-3-642-28412-0_9zbMath1278.68202WikidataQ57389356 ScholiaQ57389356MaRDI QIDQ2890327

Michael Kohlhase, Florian Rabe, Till Mossakowski, Fulya Horozal, Mihai Codescu

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_9

Mathematics Subject Classification ID

68Q65: Abstract data types; algebraic specification

03B40: Combinatory logic and lambda calculus

Related Items

A scalable module system

Uses Software

• Isabelle
• CASL
• Hets
• Automath
• MMT
• OMDoc
• TNTBase

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Foundations of algebraic specification and formal software development.
• Representing model theory in a type-theoretical logical framework
• Structured algebraic specifications: A kernel language
• Specifications in an arbitrary institution
• Structured theory presentations and logic representations
• Isabelle. A generic theorem prover
• The definition of Extended ML: A gentle introduction
• Logical systems for structured specifications.
• CASL reference manual. The complete documentation of the common algebraic specification language.
• Development graphs -- proof management for structured specifications
• Towards Logical Frameworks in the Heterogeneous Tool Set Hets
• Formalising foundations of mathematics
• Heterogeneous Logical Environments for Distributed Specifications
• Module algebra
• A framework for defining logics
• Institutions: abstract model theory for specification and programming
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Composing Hidden Information Modules over Inclusive Institutions
• A logical framework combining model and proof theory