scientific article; zbMATH DE number 1301739

MaRDI QIDQ4246952zbMATHFDO

Authors Wolfgang Naraschewski, Tobias Nipkow

Publication date 13 December 1999

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)

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

Cited in

(10)

• Nominal verification of algorithm \(W\)
• scientific article; zbMATH DE number 2086518 (Why is no real title available?)
• Proofs of a set of hybrid let-polymorphic type inference algorithms
• Haskell overloading is DEXPTIME-complete
• Isabelle/HOL
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• scientific article; zbMATH DE number 2043546 (Why is no real title available?)
• Certification of a type inference tool for ML: Damas-Milner within Coq
• Formal verification of algorithm \(\mathcal{W}\): the monomorphic case
• HM(X) type inference is CLP(X) solving

Describes a project that uses

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)