Certified Type Soundness, automatically!
AMPL OCaml Standard ML Makefile
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Comp5310_teaching_version
generated
repo
.gitignore
LICENSE
Makefile
README.md
alphaConversion.ml
aux.ml
canonicalForms.ml
contextualRules.ml
errorManagement.ml
errors.ml
generateLambdaProlog.ml
ldl.ml
ldlToTypedLanguage.ml
listLemmas.ml
listManagement.ml
parser.ml
preservation.ml
progress.ml
proof.ml
soundnessCertifier.ml
subtyping.ml
terms.ml
typeChecker.ml
typeCheckerPreservation.ml
typeCheckerProgress.ml
typeCheckerTypedLanguage.ml
typedLanguage.ml
values.ml

README.md

TypeSoundnessCertifier

Author: Matteo Cimini (matteo_cimini@uml.edu)
Tool tested with Abella versions 2.0.2 included to 2.0.5 included (latest version).

Quick links

Update (December 2017):

As of July 2017 (a POPL 2018 submission),

     TypeSoundnessCertifier automatically solves the POPLMark Challenge 2A!!

(i.e. the tool automatically generates the full mechanized type soundness proof for System F with bounded subtyping, from its language definition.)
See below for the reference to this example.

Teaching Version (April 2017):

A teaching version of the tool uses a much improved syntax.
Language definitions are in a single .lan file, see the stlc_cbv.lan example.
This version is in the folder "Comp5310_teaching_version" of the tool.
The teaching version has been successfully used in the context of the course Comp.5310 - Design of Programming Languages at University of Massachusetts Lowell.
Instructions to run the teaching version are contained in that folder "Comp5310_teaching_version".

Instructions


Requirements:

  • To compile, Ocaml is required.
  • Ocaml Batteries package is required: (to install, run "opam install batteries")
  • To run: the Abella proofs assistant must be installed and the command "abella" must be in the $PATH (to install, run "opam install abella")

Quick usage:

  • make
    Compilation may take 1 or 2 minutes
  • ./soundy
Output: a successful message means that
  • The tool has succesfully type checked all the language specifications in the folder "repo".
  • The tool has automatically generated Abella files (.sig, .mod, and especially .thm) in the folder "generated".
    These files contain the theorem and proof of type soundness for each language specification.
  • Abella has succesfully proof-checked all the type soundness proofs generated.
    To be precise: the command "abella" runs to "Proof Completed" on all generated .thm in the folder "generated".

To clean:

  • make cleanOnlyTool
    (removes compilation files and executable)
  • make clean
    (removes Abella files in "generated")

Examples of Spotted Design Mistakes in Languages.

Only a few relevant examples, acting on the file "fpl_cbv.mod" in the folder "repo":
(./soundy after each modification)
fpl_cbv.mod, which stands for 'functional programming language', contains the language definition for a functional language with integers, booleans, pairs, sums, lists, universal types, recursive types, fix, letrec, and exceptions (try, raise))

  • Remove line 33: step (pred (zero )) (raise (zero )).
    Error Message: "Operator pred is elimination form for the type int but does not have a reduction rule for handling one of the values of type int: value zero"
  • Replace line 33: step (pred (zero )) (raise (zero )). with step (pred (tt)) (raise (zero )).
    Error Message: "pred is an elimination form for type int, but has a reduction rule to handle tt, which is not a value of type int"
    Notice that the type system of a logical framework may not spot this error because pred accepts an expression as argument and (tt) is an expression. This error can be spotted after our high-level classification of operators.
  • Replace line 45: step (fst (pair E1 E2)) E1. with step (fst (pair E1 E2)) E2.
    The mistake here is that (fst (pair E1 E2)) does not have the type of E2 but that of E1.
    Error Message: "Reduction rule of fst for handling a value pair is not type preserving"
  • Remove line 133: % context app C e.
    Error Message: "The principal argument of the elimination form app is not declared as evaluation context, hence some programs may get stuck"
  • Remove line 134: % context app v C.
    Error Message: "Operator app has a reduction rule that requires some its arguments to be values, but these are not in evaluation contexts, hence some programs may get stuck."
  • Remove line 125: % context pair v C.
    Error Message: "Operator pair has a value declaration in which some of its arguments must be values, but are not in evaluation contexts, hence some programs may get stuck.""
  • Replace line 129: % context cons C e. with % context cons C v.
    Error Message: "Evaluation contexts have cyclic dependencies, hence some programs may get stuck"
  • Replace line 21: typeOf (cons E1 E2) (list T) :- typeOf E1 T, typeOf E2 (list T).
    with typeOf (cons E1 E2) (list T) :- typeOf E2 (list T).
    Error Message: "This typing rule does not assign a type to the expression E1: typing rule displayed"

Some Interesting Examples in the Folder "repo"