Cited in
(31)- Reasoning in Abella about structural operational semantics specifications
- Mechanized metatheory revisited
- Functions-as-constructors higher-order unification: extended pattern unification
- A proposal for broad spectrum proof certificates
- Proof checking and logic programming
- Proof checking and logic programming
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Executable relational specifications of polymorphic type systems using Prolog
- Optimizing higher-order pattern unification.
- Beluga
- lolliCoP
- Twelf
- Abella
- Bedwyr
- Minlog
- Tac
- LeoPARD
- KANREN
- miniKanren
- SPEC
- ELPI
- PRIZ
- AIspace
- The suspension notation for lambda terms and its use in metalanguage implementations
- Encoding generic judgments: preliminary results
- A two-level logic approach to reasoning about computations
- There is no best \(\beta \)-normalization strategy for higher-order reasoners
- A semantic framework for proof evidence
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- ELPI: fast, embeddable, \(\lambda \)Prolog interpreter
- Functions-as-constructors Higher-order Unification
This page was built for software: Teyjus
