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

Preprint English OPEN
Abel, Andreas; Sattler, Christian;
(2019)
  • 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.

    doi:10.1109/LICS.2001.932506.

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

    doi:10.1007/3-540-60164-3_27.

    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.

    doi:10.1093/logcom/2.3.297.

    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
    software
    ipl software on GitHub
    72%
  • Similar Research Results (1)
  • Metrics
Share - Bookmark