scientific article; zbMATH DE number 1301739

zbMATH Open0927.03025MaRDI QIDQ4246952FDOQ4246952

Authors: Wolfgang Naraschewski, Tobias Nipkow 

Publication date: 13 December 1999

Title of this publication is not available (Why is that?)

Recommendations

• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• Proofs of a set of hybrid let-polymorphic type inference algorithms
• Nominal verification of algorithm \(W\)
• Certification of a type inference tool for ML: Damas-Milner within Coq

zbMATH Keywords

simply typed lambda calculustype inference algorithmcomputation of the most general typemachine-checked proof of correctness and completenessMini-ML

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Cited In (10)

• Formal verification of algorithm \(\mathcal{W}\): the monomorphic case
• Nominal verification of algorithm \(W\)
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• HM(X) type inference is CLP(X) solving
• Title not available (Why is that?)
• Haskell overloading is DEXPTIME-complete
• Proofs of a set of hybrid let-polymorphic type inference algorithms
• Title not available (Why is that?)
• Isabelle/HOL
• Certification of a type inference tool for ML: Damas-Milner within Coq

Uses Software

• Coq
• Isabelle
• mini-ML

This page was built for publication:

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