Teyjus

swMATH21364MaRDI QIDQ33172FDOQ33172

Author name not available (Why is that?)

Cited In (17)

• 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
• 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
• Reasoning in Abella about structural operational semantics specifications

This page was built for software: Teyjus