Pages that link to "Item:Q1945914"
From MaRDI portal
The following pages link to The locally nameless representation (Q1945914):
Displaying 30 items.
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- Composition-nominative logics as institutions (Q1653557) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- HOCore in Coq (Q2945640) (← links)
- Higher-Order Modal Logics: Automation and Applications (Q2970308) (← links)
- The Role of Indirections in Lazy Natural Semantics (Q3455082) (← links)
- Constraint handling rules with binders, patterns and generic quantification (Q4592722) (← links)
- Syntactic soundness proof of a type-and-capability system with hidden state (Q4912884) (← links)
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus (Q4972064) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention (Q5022932) (← links)
- An extensible equality checking algorithm for dependent type theories (Q5028472) (← links)
- Normalization by Evaluation for Typed Weak lambda-Reduction (Q5091147) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- An extensible approach to session polymorphism (Q5741569) (← links)
- Psi-calculi in Isabelle (Q5890661) (← links)
- General Bindings and Alpha-Equivalence in Nominal Isabelle (Q5892493) (← links)
- Finitary type theories with and without contexts (Q6053849) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
- A Formal Proof of the Strong Normalization Theorem for System T in Agda (Q6118750) (← links)
- A strong call-by-need calculus (Q6135746) (← links)
- Extending a high-performance prover to higher-order logic (Q6536126) (← links)
- Manifest contracts with intersection types (Q6536305) (← links)
- Formal verifications of call-by-need and call-by-name evaluations with mutual recursion (Q6536314) (← links)
- Interactive matching logic proofs in Coq (Q6605348) (← links)