10 search results for "tag:"category: Computer Science/Lambda Calculi""

Showing 1 - 10
  1. coq-cfgv

    No documentation

    Generic Proofs about Alpha Equality and Substitution
    keyword: generic programming keyword: variable bindings keyword: context free grammars keyword: substitution keyword: alpha equality keyword: equivariance category: Computer Science/Lambda Calculi
    Abhishek <abhishek.anand.iitg@gmail.com> [http://www.cs.cornell.edu/~aa755/] Vincent Rahli <vincent.rahli@gmail.com> [http://www.cs.cornell.edu/~rahli/]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  2. coq-dblib

    No documentation

    Dblib
    keyword: abstract syntax keyword: binders keyword: de Bruijn indices keyword: shift keyword: lift keyword: substitution category: Computer Science/Lambda Calculi
    Francois Pottier <francois.pottier@inria.fr> [http://gallium.inria.fr/~fpottier/]
    8.8.0
    GPL
    Used by 0 other packages
    06 Feb 2019
  3. coq-domain-theory

    No documentation

    Elements of Domain Theory
    keyword: Concrete Domains category: Computer Science/Lambda Calculi
    Gilles Kahn
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  4. coq-lambda

    No documentation

    Residual Theory in Lambda-Calculus
    keyword: pure lambda-calculus keyword: confluence keyword: parallel-moves lemma keyword: Lévy's Cube Lemma keyword: Church-Rosser keyword: residual keyword: Prism theorem category: Computer Science/Lambda Calculi
    Gérard Huet
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  5. coq-lazy-pcf

    No documentation

    Subject Reduction for Lazy-PCF
    keyword: functional programming keyword: lazy evaluation keyword: operational semantics keyword: type soundness keyword: normal forms category: Computer Science/Lambda Calculi
    Amy Felty Jill Seaman
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  6. coq-lc

    No documentation

    Modules over monads and lambda-calculi
    keyword: modules keyword: monads keyword: category keyword: lambda calculus keyword: higher-order syntax category: Computer Science/Lambda Calculi date: 2006-01-12 date: 2008-09-9
    André Hirschowitz <ah@math.unice.fr> [http://math.unice.fr/~ah/] Marco Maggesi <maggesi@math.unifi.it> [http://www.math.unifi.it/~maggesi/]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  7. coq-param-pi

    No documentation

    Coding of a typed monadic pi-calculus using parameters for free names
    keyword: Pi-Calculus category: Computer Science/Lambda Calculi date: 1998-09-30
    Loïc Henry-Gréard
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  8. coq-pts

    No documentation

    A formalisation of Pure Type Systems
    keyword: pure type systems keyword: metatheory category: Computer Science/Lambda Calculi date: 2007-03
    Bruno Barras
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  9. coq-subst

    No documentation

    The confluence of Hardin-Lévy lambda-sigma-lift-calcul
    keyword: lambda-sigma-lift-calculus keyword: explicit substitution keyword: Newman's lemma keyword: Yokouchi's lemma keyword: confluence keyword: rewriting category: Computer Science/Lambda Calculi
    Amokrane Saïbi
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  10. 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