Skip to content

COCTI/certint-amb

ambivalent
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code
This branch is 176 commits ahead, 4 commits behind garrigue:master.

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.

A Certified Interpreter for ML with Structural Polymorphism

Jacques Garrigue, updated April 2020

The files in this archive contain a proof of type soundness for structural polymorphism based on local constraints [1], together with soundness and principality of the type inference algorithm, and a certified interpreter. See the support page for detailed information.

I started from a proof of type soundness for core ML by Arthur Chargueraud, which accompanied "Engineering formal metatheory" [2]. The library files (Lib_* and Metatheory*) are almost untouched. For compatibility we also copied FSetList.v from Coq 8.2.

The new files are as follows.

  • Metatheory_SP: new generic lemmas used in developments
  • Cardinal: lemmas about finite set cardinals
  • ML_SP_Definitions: basic definitions
  • ML_SP_Infrastructure: structural lemmas on kinds and types
  • ML_SP_Soundness: lemmas on derivations and proof of type soundness
  • ML_SP_Eval: proof of type soundness for a stack-based evaluator
  • ML_SP_Rename: renaming lemmas, and Gc elimination
  • ML_SP_Unify: soundness and completeness of unification
  • ML_SP_Inference: soundness and principality of type inference
  • ML_SP_Domain: instantiation of all the above proofs to polymorphic variants
  • ML_SP_Unify/Inference_wf: termination counters are in Prop

Of the above, Definitions, Infrastructure and Soundness are base on the core ML proof, but were heavily modified. Eval, Unify, Inference and Domain are completely new.

All the above development were checked with coq 8.11.0. (Porting to 8.11.0 is the only change wrt. the version of september 2010) You can compile them with "sh build.sh"

You can also play with the type checker. It does not work inside Coq at this point, but you should compile typinf.mli and typinf.ml (obtained by running Extraction.v), and look at use_typinf.ml for how to use them. (It contains a number of petty printers and conversion functions that make things easier).

Here are all the steps: (the first 3 steps are optional)

$ sh mkmakefile.sh
$ make Extraction.vo
$ make html
$ ocamlc -c typinf.mli
$ ocamlc -c typinf.ml
$ ocaml
        Objective Caml version ...
# #use "use_typinf.ml";;

[1] Jacques Garrigue: A Certified Interpreter of ML with Structural Polymorphism and Recursive Types. Mathematical Structures in Computer Science, November 2014, pages 1-25. Earlier version presented at APLAS'10, Shanghai, China, November 2010. link

[2] Brian Aydemir, Arthur Chargueraud, Benjamin C. Pierce, Randy Pollack and Stephanie Weirich: Engineering Formal Metatheory. POPL'08. link

About

A Certified Interpreter for ML with Ambivalent Types

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Coq 99.8%
  • Shell 0.2%