The following pages link to Elf (Q33169):
Displaying 46 items.
- A Maude environment for CafeOBJ (Q520244) (← links)
- Forum: A multiple-conclusion specification logic (Q671512) (← links)
- Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
- A framework for proof systems (Q707742) (← links)
- Verifying termination and reduction properties about higher-order logic programs (Q850496) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← 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)
- Efficient resource management for linear logic proof search (Q1575929) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- Program development schemata as derived rules (Q1583853) (← links)
- Automated techniques for provably safe mobile code. (Q1853627) (← links)
- Structural cut elimination. I: Intuitionistic and classical logic (Q1854335) (← links)
- A note on the proof theory of the \(\lambda \Pi\)-calculus (Q1891931) (← links)
- Twenty years of rewriting logic (Q1931904) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Logical frameworks (Q2751369) (← links)
- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax (Q2938052) (← links)
- (Q3024905) (← links)
- Programming Inductive Proofs (Q3058448) (← links)
- A modal analysis of staged computation (Q3196622) (← links)
- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation (Q3613406) (← links)
- (Q4222777) (← links)
- (Q4222859) (← links)
- (Q4249901) (← links)
- (Q4264727) (← links)
- A module system for a programming language based on the LF logical framework (Q4399511) (← links)
- A Linear Spine Calculus (Q4444935) (← links)
- (Q4499196) (← links)
- A natural deduction approach to dynamic logic (Q4647578) (← links)
- (Q4823135) (← 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)
- Representing proof transformations for program optimization (Q5210798) (← links)
- Decidable higher-order unification problems (Q5210802) (← links)
- Elf: A meta-language for deductive systems (Q5210815) (← links)
- Higher-order pattern complement and the strict λ-calculus (Q5267440) (← links)
- Mathematical Knowledge Management (Q5313058) (← links)
- The practice of logical frameworks (Q5878905) (← links)
- Primitive recursion for higher-order abstract syntax (Q5958752) (← links)
