Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
From MaRDI portal
Publication:3452250
DOI10.1145/964001.964007zbMath1325.68045OpenAlexW2140892577MaRDI QIDQ3452250
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
normalisationtyped lambda calculustype-directed partial evaluationGrothendieck logical relationsstrong sums
Related Items
Normalization by evaluation and algebraic effects, Semantic analysis of normalisation by evaluation for typed lambda calculus, Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation, On Normalization by Evaluation for Object Calculi, Relative full completeness for bicategorical Cartesian closed structure, On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation, Delimited control in OCaml, abstractly and concretely, A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators, A static simulation of dynamic delimited control, Remarks on isomorphisms in typed lambda calculi with empty and sum types, Typed Applicative Structures and Normalization by Evaluation for System F ω, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages, The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
