Pages that link to "Item:Q2871861"
From MaRDI portal
The following pages link to Nominal reasoning techniques in Coq (extended abstract) (Q2871861):
Displaying 16 items.
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- Nominal abstraction (Q617715) (← links)
- Nominal techniques in Isabelle/HOL (Q928672) (← links)
- A formalized general theory of syntax with bindings (Q1687739) (← links)
- Completeness in PVS of a nominal unification algorithm (Q1744405) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols (Q1744440) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols (Q2424886) (← links)
- (Q4535076) (← links)
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention (Q5022932) (← links)
- Deep Generation of Coq Lemma Names Using Elaborated Terms (Q5048996) (← links)
- Encoding natural semantics in Coq (Q5096388) (← links)
- Automated Deduction – CADE-20 (Q5394605) (← links)
- Nominal Sets in Agda - A Fresh and Immature Mechanization (Q6118749) (← links)