Structured theory presentations and logic representations

DOI10.1016/0168-0072(94)90009-4zbMath0809.03019OpenAlexW1969510795MaRDI QIDQ1326777

Robert Harper, Andrzej Tarlecki, Donald Sannella

Publication date: 29 March 1995

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(94)90009-4

zbMATH Keywords

consequence relationsbuilding proof systems in a structured waylogical framework for structured theory presentationrepresentation of one logical system in another

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)

Related Items (17)

Lax Theory Morphisms ⋮ A Proof Theoretic Interpretation of Model Theoretic Hiding ⋮ Towards Logical Frameworks in the Heterogeneous Tool Set Hets ⋮ Formal Logic Definitions for Interchange Languages ⋮ Proof systems for structured algebraic specifications: An overview ⋮ Functorial semantics of first-order views ⋮ Essential concepts of algebraic specification and program development ⋮ A scalable module system ⋮ Proof systems for structured specifications with observability operators ⋮ Representing model theory in a type-theoretical logical framework ⋮ A logical framework combining model and proof theory ⋮ Representing Model Theory in a Type-Theoretical Logical Framework ⋮ Property-oriented semantics of structured specifications ⋮ Formalising foundations of mathematics ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Logical systems for structured specifications. ⋮ The practice of logical frameworks

Uses Software

• Nuprl
• Automath
• Elf
• Cambridge LCF

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• Simple consequence relations
• Some fundamental algebraic tools for the semantics of computation. I. Comma categories, colimits, signatures and theories
• Structured algebraic specifications: A kernel language
• Toward formal development of programs from algebraic specifications: Implementations revisited
• Generalized algebraic theories and contextual categories
• Specifications in an arbitrary institution
• Some fundamental algebraic tools for the semantics of computation. III: Indexed categories
• Toward formal development of programs from algebraic specifications: Parameterisation revisited
• Synchronization trees
• Edinburgh LCF. A mechanized logic of computation
• Completeness of Proof Systems for Equational Specifications
• Logic and Computation
• On the Theory of Specification, Implementation, and Parametrization of Abstract Data Types
• Data Type Specification: Parameterization and the Power of Specification Techniques
• A calculus for the construction of modular prolog programs
• Abstract data types and software validation
• Institutions: abstract model theory for specification and programming
• A module system for a programming language based on the LF logical framework
• Logic representation in LF
• Toward formal development of programs from algebraic specifications: Model-theoretic foundations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Structured theory presentations and logic representations