GitHub - ezgicicek/BiRelCost: Bidirectional Type Checking for Relational Properties

ezgicicek / BiRelCost Public

Notifications You must be signed in to change notification settings
Fork 0
Star 5

Bidirectional Type Checking for Relational Properties

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 4 Commits
examples		examples
src		src
INSTALL		INSTALL
LICENSE		LICENSE
Makefile		Makefile
NOTES		NOTES
README		README
birel.why		birel.why

Repository files navigation

BiRelCost : Bidirectional Type Analysis for Relational Costs
------------------------------------------------------------- 

This repository implements a bidirectional type checker for a
refinement type and effect system.

See INSTALL for directions for compiling and running BiRelCost and its test framework.

See NOTES for detailed notes on notation, troubleshooting and misc.

This software uses why3 0.87.3 and alt-ergo 1.30.

What is where?
-----------------------------
- all the OCaml source is in src/
  * birel.ml [Main file]
  * tycheck.ml [Core typechecking functor]
  * binary.ml  [Binary typechecking engine]
  * unary.ml   [Unary typechecking engine]
  * test.ml    [Test framework]
- example programs are in examples/

- why theory file, containing all the necessary lemmas for Why3, is
  'birel.why'