Certification of a type inference tool for ML: Damas-Milner within Coq

DOI10.1023/A:1006285817788zbMath0943.68151MaRDI QIDQ1961918

Catherine Dubois, Valérie Ménissier-Morain

Publication date: 30 January 2000

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

formal proofCoq proofML type inference algorithm

Mathematics Subject Classification ID

Related Items (1)

A certified implementation of ML with structural polymorphism and recursive types

Uses Software

• Coq
• ML

This page was built for publication: Certification of a type inference tool for ML: Damas-Milner within Coq