Ωmega is a purely functional programming language and a proof system

Conceived and implemented by Tim Sheard and his students, Ωmega is a cross between a purely functional programming language and a theorem prover. The syntax is borrowed from Haskell and has been moderately extended. Ωmega offers these features: default strict evaluation laziness on demand type-level functions kind system with user-definable kinds at any level level polymorphism theorems can be formulated as types and proven with values (Curry-Howard Correspondence) GADT syntax for datatypes singleton types (emulating dependent types) custom syntax for recurring datatype patterns metaprogramming facilities staging constructs freshness Non-features (yet) termination of the logic fragment type classes (ad-hoc polymorphism) compiled binaries efficient execution debugging

distr
Auxillary.hs
Bind.hs
DepthFirstSearch.hs
Monads.hs
SCC.hs
StdTokenDef.hs
ParseError.hs
ParseExpr.hs
Parser.hs
ParserAll.hs
ParseToken.hs
TokenDefExample.hs
CommentDefExample.hs
ParserDef.hs
PrimParser.hs
CommentDef.hs
Encoding.hs
Infer.hs
LangEval.hs
Main.hs
RankN.hs
Syntax.hs
tests.prg
TokenDef.hs
Toplevel.hs
Value.hs
Manual.hs
Commands.hs
Narrow.hs
NarrowData.hs
Cooper.hs
SyntaxExt.hs
PureReadline.hs
Version.hs
LangPrelude.prg
Parsing.prg
LICENSE.txt
Makefile
OmegaManual.pdf
OmegaManual.ps