The following pages link to (Q4535076):
Displaying 13 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 π-Calculus in Isabelle/HOL using Permutations (Q2841231) (← links)
- Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. (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)
