Cited in
(75)- Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
- Higher-order superposition for dependent types
- Programming inductive proofs. A new approach based on contextual types
- Program development schemata as derived rules
- scientific article; zbMATH DE number 2185713 (Why is no real title available?)
- Efficient resource management for linear logic proof search
- scientific article; zbMATH DE number 1348473 (Why is no real title available?)
- Verifying termination and reduction properties about higher-order logic programs
- The practice of logical frameworks
- A modal analysis of staged computation
- Isabelle's metalogic: formalization and proof checker
- scientific article; zbMATH DE number 1231543 (Why is no real title available?)
- Proof-search in type-theoretic languages: An introduction
- A graph-theoretic approach to sequent derivability in the Lambek calculus
- Lolli
- Higher-order pattern complement and the strict \(\lambda\)-calculus
- scientific article; zbMATH DE number 2110615 (Why is no real title available?)
- Logical frameworks
- A notation for lambda terms. A generalization of environments
- scientific article; zbMATH DE number 1497779 (Why is no real title available?)
- Automated techniques for provably safe mobile code.
- scientific article; zbMATH DE number 1303348 (Why is no real title available?)
- TALP
- lolliCoP
- HiLog
- CoFI
- 2OBJ
- Automath
- ALF
- PAGODA
- LEGO
- K-Maude
- DDebugger
- CARIBOO
- vlogsl
- Pesca
- A natural deduction approach to dynamic logic
- K-Java
- KJS
- CafeInMaude
- KANREN
- SPEC
- SymPLFIED
- TIL
- CITP
- SKIL
- Light-weight Containers
- MiniML
- PRIZ
- Cambridge LCF
- Representing proof transformations for program optimization
- Metamath Zero
- A Linear Spine Calculus
- Using typed lambda calculus to implement formal systems on a machine
- A module system for a programming language based on the LF logical framework
- A linear logical framework
- A note on the proof theory of the \(\lambda \Pi\)-calculus
- scientific article; zbMATH DE number 1231474 (Why is no real title available?)
- Mechanized metatheory revisited
- A formalization and proof checker for Isabelle's metalogic
- Implementing tactics and tacticals in a higher-order logic programming language
- Unification under a mixed prefix
- Decidable higher-order unification problems
- Structural cut elimination. I: Intuitionistic and classical logic
- A Maude environment for CafeOBJ
- Elf: A meta-language for deductive systems
- Linear unification of higher-order patterns
- Primitive recursion for higher-order abstract syntax
- Forum: A multiple-conclusion specification logic
- Structured theory presentations and logic representations
- Mathematical Knowledge Management
- Programming type-safe transformations using higher-order abstract syntax
- Unification with extended patterns
- Twenty years of rewriting logic
- A framework for proof systems
This page was built for software: Elf
