The following pages link to (Q4012879):
Displaying 32 items.
- Elf (Q33169) (← links)
- Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
- Verifying termination and reduction properties about higher-order logic programs (Q850496) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- Unification with extended patterns (Q1274966) (← links)
- Implementing tactics and tacticals in a higher-order logic programming language (Q1311396) (← links)
- Structured theory presentations and logic representations (Q1326777) (← links)
- A linear logical framework (Q1400718) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Program development schemata as derived rules (Q1583853) (← links)
- Fuzzy types: A framework for handling uncertainty about types of objects (Q1594851) (← links)
- TWAM: a certifying abstract machine for logic programs (Q1629962) (← links)
- Automated techniques for provably safe mobile code. (Q1853627) (← links)
- Structural cut elimination. I: Intuitionistic and classical logic (Q1854335) (← links)
- Higher-order substitutions (Q1854398) (← links)
- A note on the proof theory of the \(\lambda \Pi\)-calculus (Q1891931) (← links)
- A Representation of Fω in LF (Q2841235) (← links)
- Programmed Strategies for Program Verification (Q2864527) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- A Graph-Theoretic Approach to Sequent Derivability in the Lambek Calculus (Q4923572) (← links)
- Linear unification of higher-order patterns (Q5044750) (← links)
- Higher-order superposition for dependent types (Q5055856) (← links)
- Modular AC unification of higher-order patterns (Q5096303) (← links)
- Higher order disunification: Some decidable cases (Q5096304) (← links)
- In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming (Q5108530) (← links)
- Representing proof transformations for program optimization (Q5210798) (← links)
- Decidable higher-order unification problems (Q5210802) (← links)
- Elf: A meta-language for deductive systems (Q5210815) (← links)
- The practice of logical frameworks (Q5878905) (← links)
- Primitive recursion for higher-order abstract syntax (Q5958752) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
- Representing unification in a logical framework (Q6560164) (← links)
