Forum: A multiple-conclusion specification logic

DOI10.1016/0304-3975(96)00045-XzbMath0872.68019MaRDI QIDQ671512

Dale A. Miller

Publication date: 27 February 1997

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

Mathematics Subject Classification ID

Logic programming (68N17)

Related Items

MELL in the calculus of structures, Unnamed Item, Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols, Logical approximation for program analysis, A Survey of the Proof-Theoretic Foundations of Logic Programming, Encoding transition systems in sequent calculus, Towards substructural property-based testing, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, Unnamed Item, Unnamed Item, Focusing in Linear Meta-logic, Relating State-Based and Process-Based Concurrency through Linear Logic, On the Relations between Disjunctive and Linear Logic Programming, Encryption as an abstract data-type, Specifying Proof Systems in Linear Logic with Subexponentials, Proofs as computations in linear logic, A framework for proof systems, On structuring proof search for first order linear logic, Non-commutative proof construction: a constraint-based approach, Relating state-based and process-based concurrency through linear logic (full-version), Reasoning in Abella about Structural Operational Semantics Specifications, Least and Greatest Fixed Points in Linear Logic, True Concurrency of Deep Inference Proofs, Expanding the Realm of Systematic Proof Theory, Formalizing Operational Semantic Specifications in Logic, Subexponentials in non-commutative linear logic, On the algebraic structure of declarative programming languages, Focusing and polarization in linear, intuitionistic, and classical logics, Encoding Generic Judgments, On the intuitionistic force of classical search, Connection methods in linear logic and proof nets construction, Efficient resource management for linear logic proof search, Cut-elimination for a logic with definitions and induction, Proof-search in type-theoretic languages: An introduction, On linear logic planning and concurrency, Formalization of metatheory of the Quipper quantum programming language in a linear logic

Uses Software

• ML
• Elf
• Lolli

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• On the unity of logic
• Using typed lambda calculus to implement formal systems on a machine
• A calculus of mobile processes. I
• Implementing tactics and tacticals in a higher-order logic programming language
• Logic programming in a fragment of intuitionistic linear logic
• The foundation of a generic theorem prover
• Uniform proofs as a foundation for logic programming
• Logic Programming with Focusing Proofs in Linear Logic
• A framework for defining logics
• On goal-directed provability in classical logic
• A logical analysis of modules in logic programming