Call-By-Push-Value - A Functional/Imperative Synthesis

Call-by-push-value is a programming language paradigm that, surprisingly, breaks down the call-by-value and call-by-name paradigms into simple primitives. This monograph, written for graduate students and researchers, exposes the call-by-push-value structure underlying a remarkable range of semantics, including operational semantics, domains, possible worlds, continuations and games.

Table des matières

I Language.- 1. Call-By-Value and Call-By-Name.- 2. Call-By-Push-Value: A Subsuming Paradigm.- 3. Complex Values and Equational Theory.- 4. Recursion and Infinitely Deep CBPV.- II Concrete Semantics.- 5. Simple Models of CBPV.- 6. Possible World Model for Cell Generation.- 7. Jump-With-Argument.- 8. Pointer Games.- III Categorical Semantics.- 9. Semantics in Element Style.- 10. All Models are Categorical Models.- 11. Representing Objects.- IV Conclusions.- 12. Conclusions, Comparisons and Further Work.- Appendices.- Technical Treatment of CBV and CBN.- A.1 The Jumbo ?-Calculus.- A.1.1. Introduction.- A.1.2. Tuple Types.- A.1.3. Function Types.- A.2 Languages and Tranlations.- A.3 Call-By-Value.- A.3.1. Coarse-Grain Call-By-Value.- A.3.2. Fine-Grain Call-By-Value.- A.3.3. From CG-CBV To FG-CBV.- A.4 Call-By-Name.- A.5 The Lazy Paradigm.- A.6 Subsuming FG-CBV and CBN.- A.6.1 From FG-CBV to CBPV.- A.6.2 From CBPV Back to FG-CBV.- A.6.3 From CBN to CBPV.- A.6.4 From CBPV back To CBN.- Models In The Style Of Power-Robinson.- B.1 Intoduction.- B.2 Actions of Monoidal Categories.- B.3 Freyd Categories.- B.4 Judgement Model.- B.5 Enrichment.- B.6 Connectives.- B.7 Modelling CBPV.- B.8 The Full Reflection.- B.9 Theories.- B.10 Conservativity.- References.

Résumé

Call-by-push-value is a programming language paradigm that, surprisingly, breaks down the call-by-value and call-by-name paradigms into simple primitives. This monograph, written for graduate students and researchers, exposes the call-by-push-value structure underlying a remarkable range of semantics, including operational semantics, domains, possible worlds, continuations and games.

Détails du produit

• Auteurs: P. B. Levy, P.B. Levy, Paul Blain Levy
• Edition: Springer Netherlands
• Langues: Anglais
• Format d'édition: Livre Relié
• Sortie: 14.04.2009
• EAN: 9781402017308
• ISBN: 978-1-4020-1730-8
• Pages: 352
• Poids: 770 g
• Illustrations: XLI, 352 p.
• Thèmes: Semantics Structures in Computation; Semantic Structures in Computa; Semantics Structures in Computation; Semantic Structures in Computa; Semantics Structures in Comput
• Catégories: Sciences naturelles, médecine, informatique, technique > Mathématiques > Arithmétique, algèbre; Algebra, C, computer science, Mathematics of Computing, Programming Languages, Compilers, Interpreters, Mathematical theory of computation, Computer science—Mathematics, Maths for computer scientists, Mathematical foundations, Category theory (Mathematics), Category Theory, Homological Algebra, Homological algebra, Compilers & interpreters, Programming languages (Electronic computers), Compilers and Interpreters