Formal verification of algorithm W: the monomorphic case

DOI10.1007/BFB0105414MaRDI QIDQ6567723zbMATH OpenFDO

Authors Dieter Nazareth, Tobias Nipkow

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105414

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• Nominal verification of algorithm \(W\)
• scientific article; zbMATH DE number 1301739
• A mechanized textbook proof of a type unification algorithm
• Certification of a type inference tool for ML: Damas-Milner within Coq

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A theory of type polymorphism in programming
• Basic polymorphic typechecking
• scientific article; zbMATH DE number 2185673 (Why is no real title available?)
• scientific article; zbMATH DE number 4051569 (Why is no real title available?)
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 512787 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Isabelle. A generic theorem prover
• The Principal Type-Scheme of an Object in Combinatory Logic
• Type inference for polymorphic references
• Type Reconstruction for Type Classes

This page was built for publication: Formal verification of algorithm \(\mathcal{W}\): the monomorphic case

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