3 search results for "tag:"category: Miscellaneous/Extracted Programs/Type checking unification and normalization""

Showing 1 - 3
  1. coq-coq-in-coq

    No documentation

    A formalisation of the Calculus of Construction
    keyword: calculus of constructions category: Mathematics/Logic/Type theory category: Miscellaneous/Extracted Programs/Type checking unification and normalization
    Bruno Barras
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  2. coq-founify

    No documentation

    Correctness and extraction of the unification algorithm
    keyword: First-order Unification keyword: Robinson category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category: Miscellaneous/Extracted Programs/Type checking unification and normalization
    Jocelyne Rouyer
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  3. coq-tait

    No documentation

    A normalization proof a la Tait for simply-typed lambda-calculus
    keyword: normalization keyword: lambda calculus keyword: extraction keyword: Tait proof keyword: normalization by evalution keyword: type theory category: Mathematics/Logic/Type theory category: Computer Science/Lambda Calculi category: Miscellaneous/Extracted Programs/Type checking unification and normalization date: 2004
    Pierre Letouzey Helmut Schwichtenberg
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019