Proving ML type soundness within Coq

DOI10.1007/3-540-44659-1_9MaRDI QIDQ2754040zbMATH OpenFDO

Authors Catherine Dubois

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44659-1_9

Mathematics Subject Classification ID

Recommendations

• Certification of a type inference tool for ML: Damas-Milner within Coq
• A very modal model of a modern, major, general type system
• A Sound Semantics for OCaml light
• Synthesis of ML programs in the system Coq
• Types for Proofs and Programs

Cited in

(11)

• Certification of a type inference tool for ML: Damas-Milner within Coq
• Testing your (static analysis) truths
• Executable relational specifications of polymorphic type systems using Prolog
• Rule-based operational semantics for an imperative language
• ML typing, explicit polymorphism and qualified types
• Practical Proof Search for Coq by Type Inhabitation
• A Sound Semantics for OCaml light
• Types for Proofs and Programs
• A certified implementation of ML with structural polymorphism and recursive types
• Towards substructural property-based testing
• A type soundness proof for variables in LCF ML

Describes a project that uses

Uses Software

• Isabelle/HOL
• Coq

This page was built for publication: Proving ML type soundness within Coq

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