claire

A simple proof assistant

MIT License

Stars

6

View Code on GitHub

Ecosystems: Haskell

Claire

A simple proof assistant based on LK

Build

stack
ghc >= 8

$ git clone https://github.com/myuon/claire
$ cd claire
$ stack build

Run proofchecker

$ stack exec claire lib/hol.cl
= Constants =
("all",ArrT (ArrT (VarT "'a") (ConT "bool" [])) (ConT "bool" []))
...
= Proved Theorems =
("Curry",(Pred "?P" [] :==>: (Pred "?Q" [] :==>: Pred "?R" [])) :==>: ((Pred "?P" [] :/\: Pred "?Q" []) :==>: Pred "?R" []))
...

Run interactive shell

$ stack exec claire
=========================
=== Welcome to Claire ===
=========================

Try proving!

=========================
=== Welcome to Claire ===
=========================

decl>theorem id: a ==> a

[] |- [Pred "a" [] :==>: Pred "a" []]
command>apply ImpR

[Pred "a" []] |- [Pred "a" []]
command>apply I

decl>print_proof
= proof of the previous theorem =
proof
  apply ImpR
  apply I
qed

See Parser.y for complete syntax.

Related Projects

haskell-proofs

Examples using dependent types for mathematical proofs at the type level

cha

A port of miniprl to Haskell with co-/inductive types bolted on the side.

hpp

hpp - A Haskell Preprocessor

Oclis

The obvious CLI specification format. You define the spec, Oclis generates the code! Support for ...

free-est

mini-haskell

A self-hosting mini Haskell compiler with a mini C runtime.

theorem-proving-template

Template repo for theorem proving in Liquid Haskell

Lecturas_GLC

Readings on computational logic, interactive theorem proving and functional programming.

h

effects

An implementation of "Freer Monads, More Extensible Effects".

ghc-compiler-notes

A collection of Notes on GHC

write-you-a-haskell

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)

05 Jan 2015 3,341

hs-to-coq

Convert Haskell source code to Coq source code.