swMATH21364MaRDI QIDQ33172FDOQ33172
Author name not available (Why is that?)
Official website: http://teyjus.cs.umn.edu/
Cited In (30)
- 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
- Optimizing higher-order pattern unification.
- Executable relational specifications of polymorphic type systems using Prolog
- Beluga
- Twelf
- Abella
- Bedwyr
- Minlog
- Tac
- LeoPARD
- KANREN
- miniKanren
- SPEC
- ELPI
- PRIZ
- The suspension notation for lambda terms and its use in metalanguage implementations
- AIspace
- 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
- Reasoning in Abella about structural operational semantics specifications
This page was built for software: Teyjus
