@hackage / dedukti

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

Latest1.1.4

About

Metadata

  • Last updated , by MathieuBoespflug
  • License LicenseRef-GPL
  • Categories Compilers and Interpreters

  • Maintained by: Mathieu Boespflug <mboes@lix.polytechnique.fr>

  • Lottery factor: 0

Links

Installation

This package uses the Custom cabal build type

Package Flags

Use the -f option with cabal commands to enable flags

    test (off by default)

    Compile test harness (requires test-framework).

Readme

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.