Nominal verification of algorithm W

MaRDI QIDQ3400637zbMATH OpenFDO

Authors Christian Urban, Tobias Nipkow

Publication date 5 February 2010

zbMATH Keywords

Isabelle/HOLNominal Datatype Package

Mathematics Subject Classification ID

Logic programming (68N17) Functional programming and lambda calculus (68N18) Nonnumerical algorithms (68W05) Analysis of algorithms (68W40)

Recommendations

• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• scientific article; zbMATH DE number 1301739
• Types for Proofs and Programs
• A mechanized textbook proof of a type unification algorithm
• Formalising in nominal Isabelle Crary's completeness proof for equivalence checking

Cited in

(6)

• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• Executable relational specifications of polymorphic type systems using Prolog
• Formalising in nominal Isabelle Crary's completeness proof for equivalence checking
• scientific article; zbMATH DE number 1301739 (Why is no real title available?)
• General bindings and alpha-equivalence in Nominal Isabelle
• Formal verification of algorithm \(\mathcal{W}\): the monomorphic case

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Nominal verification of algorithm \(W\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3400637)