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