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