swMATH21361MaRDI QIDQ33169FDOQ33169
Author name not available (Why is that?)
Official website: https://www.cs.cmu.edu/~fp/elf.html
Cited In (72)
- 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
- Higher-order pattern complement and the strict \(\lambda\)-calculus
- A natural deduction approach to dynamic logic
- Lolli
- 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
- Title not available (Why is that?)
- A linear logical framework
- HiLog
- 2OBJ
- Automath
- Efficient resource management for linear logic proof search
- ALF
- PAGODA
- LEGO
- K-Maude
- DDebugger
- CARIBOO
- vlogsl
- Pesca
- Programming inductive proofs. A new approach based on contextual types
- K-Java
- KJS
- CafeInMaude
- KANREN
- SPEC
- SymPLFIED
- TIL
- CITP
- SKIL
- Light-weight Containers
- MiniML
- PRIZ
- Cambridge LCF
- Title not available (Why is that?)
- Logical frameworks
- Representing proof transformations for program optimization
- Metamath Zero
- 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
- Programming type-safe transformations using higher-order abstract syntax
- Proof-search in type-theoretic languages: An introduction
- Using typed lambda calculus to implement formal systems on a machine
- A Maude environment for CafeOBJ
- Title not available (Why is that?)
- Program development schemata as derived rules
- The practice of logical frameworks
This page was built for software: Elf
