Encoding Generic Judgments

DOI10.1016/S1571-0661(04)00279-8zbMath1268.68051OpenAlexW1503868244MaRDI QIDQ2841234

Dale A. Miller

Publication date: 24 July 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)00279-8

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Logic programming (68N17)

Uses Software

• Teyjus

Cites Work

• Forum: A multiple-conclusion specification logic
• \(\pi\)-calculus, internal mobility, and agent-passing calculi
• Modal logics for mobile processes
• A calculus of mobile processes. II
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Encoding transition systems in sequent calculus
• Cut-elimination for a logic with definitions and induction
• \(\pi\)-calculus in (Co)inductive-type theory
• The foundation of a generic theorem prover
• Uniform proofs as a foundation for logic programming
• Programming with Higher-Order Logic
• A Proof-Theoretic Approach to Logic Programming. I. Clauses as Rules
• A Proof-Theoretic Approach to Logic Programming
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Logic Programming with Focusing Proofs in Linear Logic
• Reasoning with higher-order abstract syntax in a logical framework
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item