The following pages link to Teyjus (Q33172):
Displaying 17 items.
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Proof checking and logic programming (Q2628296) (← links)
- Executable Relational Specifications of Polymorphic Type Systems Using Prolog (Q2798266) (← links)
- Reasoning in Abella about structural operational semantics specifications (Q2804943) (← links)
- Encoding generic judgments: preliminary results (Q2841234) (← links)
- A Proposal for Broad Spectrum Proof Certificates (Q3100201) (← links)
- LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners (Q3453128) (← links)
- There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners (Q3460064) (← links)
- ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter (Q3460075) (← links)
- The Suspension Notation for Lambda Terms and its Use in Metalanguage Implementations (Q4916200) (← links)
- Functions-as-constructors Higher-order Unification (Q5369491) (← links)
- Proof Checking and Logic Programming (Q5743582) (← links)
- Automated Deduction – CADE-19 (Q5900734) (← links)