A framework for defining logics
From MaRDI portal
Publication:4033837
DOI10.1145/138027.138060zbMath0778.03004MaRDI QIDQ4033837
Gordon D. Plotkin, Furio Honsell, Robert Harper
Publication date: 16 May 1993
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/1842/202
higher-order abstract syntax; logical frameworks; LF type theory; judgment as types; meta- logic for defining logics; typed \(\lambda\)-calculus with dependent types
03B70: Logic in computer science
03F35: Second- and higher-order arithmetic and fragments
03B40: Combinatory logic and lambda calculus
Related Items
Equivalences between logics and their representing type theories, Mechanizing metatheory in a logical framework, Completeness and Herbrand theorems for nominal logic, Least and greatest fixed points in intuitionistic natural deduction, Primitive recursion for higher-order abstract syntax, Subtyping dependent types, Proof-term synthesis on dependent-type systems via explicit substitutions, An induction principle for pure type systems, Forum: A multiple-conclusion specification logic, Using typed lambda calculus to implement formal systems on a machine, Theo: An interactive proof development system, Definition and basic properties of the Deva meta-calculus, Substitution in non-wellfounded syntax with variable binding, Verifying termination and reduction properties about higher-order logic programs, Simplifying proofs in Fitch-style natural deduction systems, Choices in representation and reduction strategies for lambda terms in intensional contexts, Do-it-yourself type theory, A notation for lambda terms. A generalization of environments, Type checking with universes, Dependent type system with subtyping I: Type level transitivity elimination, From constructivism to computer science, Implementing tactics and tacticals in a higher-order logic programming language, Nominalization, predication and type containment, Toward formal development of programs from algebraic specifications: Parameterisation revisited, Inductive families, A higher-order unification algorithm for inductive types and dependent types, A linear logical framework, The calculus of constructions as a framework for proof search with set variable instantiation, Proof-search in type-theoretic languages: An introduction, Program development schemata as derived rules, \(\pi\)-calculus in (Co)inductive-type theory, Amalgamation in the semantics of CASL, Transitivity in coercive subtyping, The foundation of a generic theorem prover, Automated techniques for provably safe mobile code., Structural cut elimination. I: Intuitionistic and classical logic, Higher-order substitutions, On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions, Dependent types with subtyping and late-bound overloading, A note on the proof theory of the \(\lambda \Pi\)-calculus, An approach to literate and structured formal developments, Relative properties of frame language, A type-theoretic approach to program development, On the mechanization of the proof of Hessenberg's theorem in coherent logic, A higher-order calculus and theory abstraction, Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts, Structural subtyping for inductive types with functorial equality rules, Celf – A Logical Framework for Deductive and Concurrent Systems (System Description), THF0 – The Core of the TPTP Language for Higher-Order Logic, Focusing in Linear Meta-logic, Unnamed Item, Unnamed Item
