@hackage dedukti1.1.4

A type-checker for the λΠ-modulo calculus.

Categories
- Compilers and Interpreters
License
LicenseRef-GPL
Maintainer
Mathieu Boespflug <mboes@lix.polytechnique.fr>
Links
Versions
- 1.1.4 Fri, 8 Apr 2011
- 1.1.3 Thu, 20 May 2010
- 1.1.2 Sat, 3 Apr 2010
- 1.1.1 Sat, 3 Apr 2010
- 1.1.0 Fri, 2 Apr 2010
- 1.0.3 Wed, 7 Oct 2009

Installation
Custom
In your cabal file:
Dependencies (2)
- unix >=2.3
- time >=1.1
Dependents (1)
@hackage/acme-everything

Package Flags

test

(off by default)

Compile test harness (requires test-framework).

Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo [1].

1: G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 31, 2003, pp. 33-72.

@hackage dedukti1.1.4

Categories

License

Maintainer

Links

Versions

InstallationCustom

Dependencies (2)

Dependents (1)

Package Flags

Installation
Custom