Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus

Preprint English OPEN
Abel, Andreas; Sattler, Christian;
  • Subject: Computer Science - Programming Languages | Mathematics - Logic | 03F05 | Computer Science - Logic in Computer Science | F.3.2 | F.4.1
    arxiv: Mathematics::Category Theory | Computer Science::Logic in Computer Science

We observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped with a monad that allows us to perform case distinction on neutral terms of sum type. The p... View more
  • References (29)
    29 references, page 1 of 3

    Andreas Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. PhD thesis, Ludwig-Maximilians-Universität München, 2006.

    Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In LICS'01. IEEE CS Press, 2001.


    Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In CTCS'95, volume 953 of LNCS. Springer, 1995.


    Thorsten Altenkirch and Tarmo Uustalu. Normalization by evaluation for λ→2. In FLOPS'04, volume 2998 of LNCS. Springer, 2004. doi:10.1007/978-3-540-24754-8\_19.

    Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. JLC, 2(3), 1992.


    Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In POPL'04. ACM, 2004. doi:10.1145/964001.964007.

    Freiric Barral. Decidability for non-standard conversions in lambda-calculus. PhD thesis, Ludwig-Maximilians-University Munich, 2008.

  • Related Research Results (1)
    Inferred by OpenAIRE
    ipl software on GitHub
  • Similar Research Results (1)
  • Metrics
Share - Bookmark