Skip to content

Athan13/ip-forall

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

9 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Interactive Prover Forall (ip-forall)

Implementing pi-forall.

Written in Haskell using cabal. To test the examples in Main.hs, simply run cabal build and cabal run in the directory.

The structure is as follows:

├── app
    ├── Environment.hs  // contains the typechecking monad
    ├── Main.hs         // entry point: runs `inferType` on the examples listed
    ├── Syntax.hs       // specifies the AST
    └── Typecheck.hs    // implements `inferType` and `checkType`

About

Mini implementation of pi-forall: a dependently-typed functional programming language

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors