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

DOI10.1145/964001.964007MaRDI QIDQ3452250zbMATH OpenOpenAlexFDO

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

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)

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

Cited in

(23)

• scientific article; zbMATH DE number 1722652 (Why is no real title available?)
• Normalization by evaluation and algebraic effects
• Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation
• scientific article; zbMATH DE number 2090724 (Why is no real title available?)
• 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
• The exp-log normal form of types: decomposing extensional equality and representing terms compactly
• Polarised intermediate representation of lambda calculus with sums
• 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
• Type directed partial evaluation for level-1 shift and reset
• scientific article; zbMATH DE number 2018582 (Why is no real title available?)
• scientific article; zbMATH DE number 1692906 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 3954870 (Why is no real title available?)
• 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)