2 search results for "tag:"keyword: type theory""

Showing 1 - 2
  1. coq-izf

    No documentation

    Intuitionistic Zermelo-Fraenkel Set Theory in Coq
    keyword: Intuitionistic set theory keyword: pointed graphs keyword: type theory keyword: intuitionistic choice operator keyword: set theory keyword: Zermelo-Fraenkel category: Mathematics/Logic/Set theory date: 2003-02
    Alexandre Miquel <Alexandre.Miquel@pps.jussieu.fr> [http://www.pps.jussieu.fr/~miquel]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  2. 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