Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

DOI10.1145/964001.964007zbMATH Open1325.68045OpenAlexW2140892577MaRDI QIDQ3452250FDOQ3452250

Authors: Vincent Balat, Roberto Di Cosmo, Marcelo P. Fiore 

Publication date: 11 November 2015

Published in: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/964001.964007

Recommendations

• scientific article; zbMATH DE number 2090724
• scientific article; zbMATH DE number 1722652
• scientific article; zbMATH DE number 1487847
• Extensional Rewriting with Sums
• Typeful normalization by evaluation

zbMATH Keywords

normalisationtyped lambda calculustype-directed partial evaluationGrothendieck logical relationsstrong sums

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Cited In (20)

• Title not available (Why is that?)
• Title not available (Why is that?)
• Normalization by evaluation and algebraic effects
• Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation
• Relative full completeness for bicategorical Cartesian closed structure
• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• Semantic analysis of normalisation by evaluation for typed lambda calculus
• Delimited control in OCaml, abstractly and concretely
• On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation
• A static simulation of dynamic delimited control
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators
• Title not available (Why is that?)
• Title not available (Why is that?)
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• On Normalization by Evaluation for Object Calculi
• Extensional Rewriting with Sums
• Normalization by evaluation for the lambek calculus
• Title not available (Why is that?)
• Typed Applicative Structures and Normalization by Evaluation for System F ω

This page was built for publication: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3452250)