A framework for defining logics

DOI10.1145/138027.138060zbMath0778.03004OpenAlexW1974190112MaRDI QIDQ4033837

Robert Harper, Furio Honsell, Gordon D. Plotkin

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

zbMATH Keywords

higher-order abstract syntax logical frameworks LF type theory judgment as types meta- logic for defining logics typed \(\lambda\)-calculus with dependent types

Mathematics Subject Classification ID

Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)

Related Items

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, Inductive families, TWAM: a certifying abstract machine for logic programs, Proof checking and logic programming, A note on the proof theory of the \(\lambda \Pi\)-calculus, Verifying termination and reduction properties about higher-order logic programs, Simplifying proofs in Fitch-style natural deduction systems, A higher-order calculus and theory abstraction, Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts, A higher-order unification algorithm for inductive types and dependent types, Strongly typed term representations in Coq, A canonical locally named representation of binding, Formalizing adequacy: a case study for higher-order abstract syntax, A two-level logic approach to reasoning about computations, Choices in representation and reduction strategies for lambda terms in intensional contexts, An approach to literate and structured formal developments, Morphism axioms, A notation for lambda terms. A generalization of environments, A scalable module system, Intuitionistic completeness of first-order logic, The rewriting logic semantics project: a progress report, Human rationality challenges universal logic, Twenty years of rewriting logic, Combining behavioural types with security analysis, Nominal abstraction, A formalized general theory of syntax with bindings, Making PVS accessible to generic services by interpretation in a universal format, N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker, Unifying sets and programs via dependent types, A linear logical framework, Mechanizing type environments in weak HOAS, The Mizar Mathematical Library in OMDoc: translation and applications, Semantical analysis of contextual types, A semantic framework for proof evidence, Cut elimination for a logic with induction and co-induction, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, A framework for conflict analysis of normative texts written in controlled natural language, Do-it-yourself type theory, First-order automated reasoning with theories: when deduction modulo theory meets practice, SMT proof checking using a logical framework, Relative properties of frame language, Representing model theory in a type-theoretical logical framework, Type checking with universes, Forum: A multiple-conclusion specification logic, Structure-preserving diagram operators, A formalized general theory of syntax with bindings: extended version, Binding operators for nominal sets, Proof certificates for equality reasoning, Canonical HybridLF: extending Hybrid with dependent types, On the mechanization of the proof of Hessenberg's theorem in coherent logic, A Maude environment for CafeOBJ, 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, A dependent type theory with abstractable names, External and internal syntax of the \(\lambda \)-calculus, Substitution in non-wellfounded syntax with variable binding, Amalgamation in the semantics of CASL, A framework for proof systems, Transitivity in coercive subtyping, A type-theoretic approach to program development, From LCF to Isabelle/HOL, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, Explicit Contexts in LF (Extended Abstract), Case Analysis of Higher-Order Data, Reasoning in Abella about Structural Operational Semantics Specifications, A rewriting logic approach to operational semantics, Subformula linking for intuitionistic logic with application to type theory, Harpoon: mechanizing metatheory interactively, Dependent type system with subtyping I: Type level transitivity elimination, From constructivism to computer science, The foundation of a generic theorem prover, Experiences from exporting major proof assistant libraries, Mechanized metatheory revisited, Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types., A Representation of Fω in LF, A Third-Order Representation of the λμ-Calculus, The Theory of Contexts for First Order and Higher Order Abstract Syntax, Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic, Proof assistants: history, ideas and future, The universal exponentiable arrow, The calculus of constructions as a framework for proof search with set variable instantiation, Proof-search in type-theoretic languages: An introduction, Formalization of metatheory of the Quipper quantum programming language in a linear logic, Program development schemata as derived rules, \(\pi\)-calculus in (Co)inductive-type theory, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, Logic-independent proof search in logical frameworks (short paper), 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, Implementing tactics and tacticals in a higher-order logic programming language, From the universality of mathematical truth to the interoperability of proof systems, Rensets and renaming-based recursion for syntax with bindings, Nominalization, predication and type containment, Mechanizing metatheory without typing contexts, Toward formal development of programs from algebraic specifications: Parameterisation revisited, The future of logic: foundation-independence, LF+ in Coq for "fast and loose" reasoning, Lax Theory Morphisms, A modular construction of type theories, A Proof Theoretic Interpretation of Model Theoretic Hiding, Towards Logical Frameworks in the Heterogeneous Tool Set Hets, Generic Literals, Formal Logic Definitions for Interchange Languages, Math Literate Knowledge Management via Induced Material, Inductive Beluga: Programming Proofs, Higher-order unification with dependent function types, On confluence for weakly normalizing systems, Higher-order superposition for dependent types, A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types, A Query Language for Formal Mathematical Libraries, A Realizability Interpretation for Intersection and Union Types, Implementing Cantor’s Paradise, Certificate size reduction in abstraction-carrying code, The Twelf Proof Assistant, Heterogeneous Logical Environments for Distributed Specifications, Term-Generic Logic, Translating a Dependently-Typed Logic to First-Order Logic, Mechanizing metatheory in a logical framework, The Essence of Dependent Object Types, Computational logic: its origins and applications, Structuring metatheory on inductive definitions, Proving and rewriting, Some normalization properties of martin-löf's type theory, and applications, Logic representation in LF, Encoding natural semantics in Coq, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming, POPLMark reloaded: Mechanizing proofs by logical relations, Equivalences between logics and their representing type theories, Unnamed Item, Mtac: A monad for typed tactic programming in Coq, Unnamed Item, Unnamed Item, Structural subtyping for inductive types with functorial equality rules, Extensible Datasort Refinements, Programs Using Syntax with First-Class Binders, LINCX: A Linear Logical Framework with First-Class Contexts, 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, A consistent semantics of self-adjusting computation, A logical framework combining model and proof theory, The representational adequacy of <scp>Hybrid</scp>, Reflection of formal tactics in a deductive reflection framework, Proof search with set variable instantiation in the Calculus of Constructions, A natural deduction approach to dynamic logic, Applicable Mathematics in a Minimal Computational Theory of Sets, An insider's look at LF type reconstruction: everything you (n)ever wanted to know, Representing Model Theory in a Type-Theoretical Logical Framework, Typed Multiset Rewriting Specifications of Security Protocols, Proof Checking and Logic Programming, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Introduction to Type Theory, Unnamed Item, Unnamed Item, Unnamed Item, Programming Inductive Proofs, Unnamed Item, A Foundational View on Integration Problems, Combining Source, Content, Presentation, Narration, and Relational Representation, Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions, Mechanizing proofs with logical relations – Kripke-style, The applicability of logic program analysis and transformation to theorem proving, Representing proof transformations for program optimization, Tactic theorem proving with refinement-tree proofs and metavariables, Elf: A meta-language for deductive systems, Mollusc a general proof-development shell for sequent-based logics, Unnamed Item, High-level signatures and initial semantics, The Rewriting Logic Semantics Project: A Progress Report, A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance, Refinement Types as Proof Irrelevance, Completeness and Herbrand theorems for nominal logic, Formalising foundations of mathematics, A pluralist approach to the formalisation of mathematics, A practical implementation of simple consequence relations using inductive definitions, Nuprl-Light: An implementation framework for higher-order logics, A case study in programming coinductive proofs: Howe’s method, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Flexary Operators for Formalized Mathematics, Towards Knowledge Management for HOL Light, Machine Translation and Type Theory, A Framework for Defining Logical Frameworks, Programmed Strategies for Program Verification, Proof-directed program transformation: A functional account of efficient regular expression matching, Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions, Type-Based Security for Mobile Computing Integrity, Secrecy and Liveness, Hybridizing a Logical Framework, Normalization for the Simply-Typed Lambda-Calculus in Twelf, Meta-programming With Built-in Type Equality, Specifying Properties of Concurrent Computations in CLF, Redundancy Elimination for LF, A Meta Linear Logical Framework, Imperative LF Meta-Programming, The practice of logical frameworks, Finitary type theories with and without contexts, On extensibility of proof checkers, A Survey of the Proof-Theoretic Foundations of Logic Programming, A Comparison of Type Theory with Set Theory, Checking algorithms for Pure Type Systems, The expressive power of Structural Operational Semantics with explicit assumptions, Closure under alpha-conversion, Semantics for abstract clauses, A logical framework with higher-order rational (circular) terms, Rensets and renaming-based recursion for syntax with bindings extended version, Morphism equality in theory graphs, A general framework for the semantics of type theory, Unnamed Item, Unnamed Item, Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules, 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, Scalable fine-grained proofs for formula processing