The following pages link to Substitution revisited (Q1106190):
Displaying 31 items.
- Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus (Q530864) (← links)
- Substitution operators (Q548122) (← links)
- Strong categorical datatypes II: A term logic for categorical programming (Q673963) (← links)
- External and internal syntax of the \(\lambda \)-calculus (Q968531) (← links)
- A conservative look at operational semantics with variable binding (Q1273877) (← links)
- The Qu-Prolog unification algorithm: formalisation and correctness (Q1349886) (← links)
- A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
- Variables and scopes considered formally (Q1603432) (← links)
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory (Q1744410) (← links)
- Secure mechanical verification of mutually recursive procedures (Q1887136) (← links)
- Point-free substitution (Q1924634) (← links)
- Timing and causality in process algebra (Q1924998) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda (Q2229159) (← links)
- Term-generic logic (Q2339466) (← links)
- Substitution and superstars (Q2345154) (← links)
- Formal metatheory of the lambda calculus using Stoughton's substitution (Q2358702) (← links)
- A canonical locally named representation of binding (Q2392482) (← links)
- The mechanisation of Barendregt-style equational proofs (the residual perspective) (Q2841232) (← links)
- Nominal equational logic (Q2864152) (← links)
- Foundations of Nominal Techniques: Logic and Semantics of Variables in Abstract Syntax (Q3011103) (← links)
- Marcus and Substitutivity (Q3187715) (← links)
- (Q3318749) (← links)
- Reduction Under Substitution (Q3522035) (← links)
- The Substitution Vanishes (Q3623933) (← links)
- Mechanical verification of mutually recursive procedures (Q4647514) (← links)
- On the Notion of Substitution (Q4821649) (← links)
- Full substitutability (Q5121487) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
- Simultaneous substitution in the typed lambda calculus (Q6116572) (← links)
- A Formal Proof of the Strong Normalization Theorem for System T in Agda (Q6118750) (← links)
