What people are saying - Write a reviewWe haven't found any reviews in the usual places. Related books
Contents
Common terms and phrasesAn-i arena Ax.M big-step semantics bool C-morphism cartesian category cartesian closed category categorical semantics CBN type CBPV adjunction model CBPV judgement model CBPV model CBPV+control CBV and CBN cell changestk Chap CK-machine closed value compact elements complex values computation F hc computation of type computation type continuous functions countable define Definition denotational semantics distributive coproduct diverge equational theory example exponential faithful functor FG-CBV finite function types functor category game semantics given global store induction infinitely deep interpret isomorphism jump jump-points Kleisli language letstk locally C-indexed category Moggi morphism natural transformation nonreturning command operational semantics opGr pointer game poset predomain Prop Proposition provable equality recursion representing object Scott semantics Sect semantics of types stack StkPS transform strong monad syntax thunk translation type denotes value F hv value of type value type vertex write x-calculus References to this bookFrom Google ScholarSeparation Logic for Higher-Order StoreBernhard Reus, Jan Schwinghammer Reasoning about Denotations of Recursive ObjectsJan Schwinghammer Infinite trace equivalencePaul Blain Levy - 2008 - Annals of Pure and Applied Logic A Typed Semantics of Higher-Order Store and SubtypingJan Schwinghammer References from web pagesAdjunction Models For Call-By-Push-Value With Stacks Adjunction models for call-by-push-value With stacks Call-By-Push-Value: A Subsuming Paradigm - Levy (researchindex) Call-by-push-value: A subsuming paradigm Call-by-push-value categories: Call-By-Push-Value thesis available Paul Blain Levy Papers ADJUNCTION MODELS FOR CALL-BY-PUSH-VALUE WITH STACKS 1. Introduction D: Verification methods DBLP: Paul Blain Levy Bibliographic information |