Elf
From MaRDI portal
Software:33169
swMATH21361MaRDI QIDQ33169FDOQ33169
Author name not available (Why is that?)
Cited In (46)
- Automated techniques for provably safe mobile code.
- Twenty years of rewriting logic
- Structural cut elimination. I: Intuitionistic and classical logic
- A framework for proof systems
- A Linear Spine Calculus
- Mechanized metatheory revisited
- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
- A graph-theoretic approach to sequent derivability in the Lambek calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- Unification with extended patterns
- A natural deduction approach to dynamic logic
- Title not available (Why is that?)
- Forum: A multiple-conclusion specification logic
- A notation for lambda terms. A generalization of environments
- Primitive recursion for higher-order abstract syntax
- Linear unification of higher-order patterns
- Verifying termination and reduction properties about higher-order logic programs
- A module system for a programming language based on the LF logical framework
- Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
- Title not available (Why is that?)
- A linear logical framework
- Efficient resource management for linear logic proof search
- Programming inductive proofs. A new approach based on contextual types
- Title not available (Why is that?)
- Logical frameworks
- Representing proof transformations for program optimization
- Mathematical Knowledge Management
- Isabelle's metalogic: formalization and proof checker
- A formalization and proof checker for Isabelle's metalogic
- Decidable higher-order unification problems
- A note on the proof theory of the \(\lambda \Pi\)-calculus
- Implementing tactics and tacticals in a higher-order logic programming language
- Unification under a mixed prefix
- Higher-order superposition for dependent types
- A modal analysis of staged computation
- Title not available (Why is that?)
- Elf: A meta-language for deductive systems
- Structured theory presentations and logic representations
- Proof-search in type-theoretic languages: An introduction
- Using typed lambda calculus to implement formal systems on a machine
- A Maude environment for CafeOBJ
- Higher-order pattern complement and the strict λ-calculus
- Title not available (Why is that?)
- Program development schemata as derived rules
- The practice of logical frameworks
This page was built for software: Elf