5 search results for "tag:"category: Mathematics/Logic/Type theory""

Showing 1 - 5
  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-intuitionistic-nuprl

    No documentation

    An Impredicative Model of Nuprl's Constructive Type Theory
    keyword: Nuprl keyword: computational type theory keyword: extensional type theory keyword: intuitionistic type theory keyword: Howe's computational equivalence relation keyword: Partial Equivalence Relation (PER) semantics keyword: consistency keyword: continuity keyword: bar induction category: Mathematics/Logic/Type theory
    Vincent Rahli <vincent.rahli@gmail.com> [http://www.cs.cornell.edu/~rahli/] Abhishek Anand <abhishek.anand.iitg@gmail.com> [http://www.cs.cornell.edu/~aa755/] Mark Bickford <mark.concertina@gmail.com> [http://nuprl.org/]
    8.6.0
    GPL
    Used by 0 other packages
    20 Nov 2018
  3. coq-ptsatr

    No documentation

    PTSATR
    keyword: pure type systems keyword: judgmental equality keyword: Church-Rosser keyword: confluence keyword: subject reduction keyword: pi injectivity category: Mathematics/Logic/Type theory
    Vincent Siles <vincent.siles@ens-lyon.org> [http://www.lix.polytechnique.fr/~vsiles] Hugo Herbelin <hugo.herbelin@inria.fr> [http://pauillac.inria.fr/~herbelin/]
    8.10.0
    LGPL
    Used by 1 other packages
    07 Dec 2019
  4. coq-ptsf

    No documentation

    Explicit Convertibility Proofs in Pure Type Systems
    keyword: pure type systems keyword: judgmental equality keyword: explicit equality proofs keyword: proof relevance category: Mathematics/Logic/Type theory
    Floris van Doorn <fpv@andrew.cmu.edu> [http://www.andrew.cmu.edu/user/fpv/] Herman Geuvers <herman@cs.ru.nl> [http://www.cs.ru.nl/~herman/] Freek Wiedijk <freek@cs.ru.nl> [http://www.cs.ru.nl/~freek/]
    8.10.0
    BSD
    Used by 0 other packages
    07 Dec 2019
  5. 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