The following pages link to (Q4535076):
Displaying 14 items.
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- About permutation algebras, (pre)sheaves and named sets (Q853745) (← links)
- Mechanizing type environments in weak HOAS (Q897934) (← links)
- Nominal unification (Q1882909) (← links)
- Nominal logic, a first order theory of names and binding (Q1887151) (← links)
- Nested abstract syntax in Coq (Q1945918) (← links)
- Semantical analysis of contextual types (Q2200843) (← links)
- Fresh logic: Proof-theory and semantics for FM and nominal techniques (Q2372191) (← links)
- Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts (Q2642466) (← links)
- A first-order syntax for the \(\pi\)-calculus in Isabelle/HOL using permutations (Q2841231) (← links)
- Developing (meta)theory of \(\lambda\)-calculus in the theory of contexts (Q2841233) (← links)
- The theory of contexts for first order and higher order abstract syntax (Q2841274) (← links)
- Comparing higher-order encodings in logical frameworks and tile logic (Q2841275) (← links)
- Nominal reasoning techniques in Coq (extended abstract) (Q2871861) (← links)
