lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
IN THIS PACKAGE

Libraries

This package provides the following libraries (via dune):

lambdapi.common

Documentation:

Dependencies: camlp-streams, timed, lambdapi.lplib

lambdapi.core

Documentation:

Dependencies: lambdapi.common, lambdapi.lplib, pratter, bindlib, why3

lambdapi.export

Documentation:

  • Export.Dk Export a Lambdapi signature to Dedukti.
  • Export.Hrs This module provides a function to translate a signature to the HRS format used in the confluence competition.
  • Export.Xtc This module provides a function to translate a signature to the XTC format used in the termination competition.

Dependencies: lambdapi.core, lambdapi.parsing, lambdapi.lplib

lambdapi.handle

Documentation:

Dependencies: lambdapi.core, lambdapi.parsing, lambdapi.tool

lambdapi.lplib

Documentation:

Dependencies: stdlib-shims, str, unix

lambdapi.lsp

Documentation:

Dependencies: yojson, lambdapi.pure

lambdapi.parsing

Documentation:

  • Parsing.DkBasic
  • Parsing.DkLexer
  • Parsing.DkParser
  • Parsing.DkRule
  • Parsing.DkTokens
  • Parsing.LpLexer
  • Parsing.LpParser
  • Parsing.Package
  • Parsing.Parser
  • Parsing.Pratt
  • Parsing.Pretty
  • Parsing.Scope
  • Parsing.Syntax

Dependencies: camlp-streams, lambdapi.core, menhirLib, pratter, sedlex, sedlex.ppx, lambdapi.common

lambdapi.pure

Documentation: Pure

Dependencies: camlp-streams, lambdapi.handle, lambdapi.core

lambdapi.tool

Documentation:

  • Tool.External Provides a function for calling external checkers using a Unix command.
  • Tool.Lcr Incremental verification of local confluence
  • Tool.Sr Checking that a rule preserves typing (subject reduction property).
  • Tool.Tree_graphviz Representation of trees as graphviz files.

Dependencies: lambdapi.parsing, lambdapi.core