scientific article; zbMATH DE number 1754648

zbMath0986.68016MaRDI QIDQ4535076

Marino Miculan, Furio Honsell, Ivan Scagnetto

Publication date: 12 June 2002

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2076/20760963

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

inductionhigher-order abstract syntaxlogical frameworks

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (13)

Nominal unification ⋮ Nominal logic, a first order theory of names and binding ⋮ Fresh logic: Proof-theory and semantics for FM and nominal techniques ⋮ About permutation algebras, (pre)sheaves and named sets ⋮ Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts ⋮ Mechanizing type environments in weak HOAS ⋮ Nested abstract syntax in Coq ⋮ Semantical analysis of contextual types ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations ⋮ Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types. ⋮ The Theory of Contexts for First Order and Higher Order Abstract Syntax ⋮ Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic

This page was built for publication: