Hybrid Contract Checking for OCaml
 

Our server currently does not allow interactive webpage. Examples below give an overview of what contracts and program we can deal with.

 

Examples

intro123, neg

arith, sum, max

append

zipunzip

McCarthy's 91 function

ack, fhnhn

stdlib/list.ml

riser

insertion-sort

bubble-sort

selection-sort

merge-sort

quick-sort

AVL tree

Redblack tree

 
At the moment, we give monomorphic type to parameters of a function. I was told that, in the next release of alt-ergo, an option -triggers-var will support instantiating a polymorphic variable in an axiom so that we do not have to give monomorphic type to parameters of a function.