Games and Full Abstraction for a Functional Metalanguage with Recursive Types1 Introduction.- 2 Preliminaries.- 3 Games.- 4 Rational Categories and Recursive Types.- 5 FPC and its Models.- 6 Full Abstraction.- 7 Conclusions. |
Contents
I | 1 |
II | 2 |
III | 4 |
IV | 5 |
V | 6 |
VI | 7 |
VII | 9 |
X | 14 |
XLIX | 84 |
LI | 86 |
LII | 87 |
LIII | 89 |
LV | 91 |
LVI | 92 |
LVII | 93 |
LVIII | 94 |
XI | 17 |
XII | 18 |
XIII | 27 |
XV | 29 |
XVI | 31 |
XVII | 34 |
XVIII | 36 |
XIX | 37 |
XX | 38 |
XXI | 39 |
XXII | 40 |
XXIV | 41 |
XXV | 42 |
XXVI | 44 |
XXVIII | 46 |
XXX | 47 |
XXXI | 49 |
XXXII | 50 |
XXXIII | 51 |
XXXIV | 53 |
XXXV | 57 |
XXXVI | 59 |
XXXVII | 60 |
XXXVIII | 63 |
XXXIX | 64 |
XL | 67 |
XLI | 68 |
XLII | 71 |
XLIV | 72 |
XLV | 75 |
XLVI | 78 |
XLVII | 82 |
Other editions - View all
Games and Full Abstraction for a Functional Metalanguage with Recursive Types Guy McCusker No preview available - 2011 |
Games and Full Abstraction for a Functional Metalanguage with Recursive Types Guy McCusker No preview available - 2012 |
Common terms and phrases
A-calculus a₁ Abramsky admissible action algebra B₁ bisimulation bracketing condition cartesian closed category category of games category theory compact strategies component composition computational adequacy construction cpo-enriched definable definition denotational semantics dist endomorphism enriched category equivalence finite types fully abstract fully abstract model game semantics games model given hom-sets id[r inductive hypothesis inductive step initial move innocent strategy interpretation intro(M IP-categories isomorphism justified sequence language least endomorphism least homomorphism least upper bound Lemma linear logic M₁ metalanguage model of FPC morphisms notion O-move objects operational semantics outl P-move pending question Player R-relation rational category rational chain rational IP-functor recursive types relational structure result satisfies strict sum sum types Suppose symmetric monoidal T₁ Theorem theory trivial variables view function visibility condition weak coproduct well-opened µT.T
Popular passages
Page 180 - JME Hyland and C.-HL Ong. On full abstraction for PCF: I, II and III.
Page 181 - On the adequacy of program dependence graphs for representing programs," in Conference Record of the 15th Annual ACM Symposium on Principles of Programming Languages, San Diego, California, pp. 146-157, January 1988. [8] J. Ferrante, K. Ottenstein, and J. Warren, "The program dependence graph and its use in optimization," ACM Transactions on Programming Languages and Systems, vol.
Page 184 - BA Trakhtenbrot, JY Halpern, and AR Meyer. From denotational to operational and axiomatic semantics for ALGOL-like languages: an overview.
Page 176 - Mackie, and R. Nagarajan, editors, Theory and Formal Methods 1994: Proceedings of the second Imperial College Department of Computing Workshop on Theory and Formal Methods, pages 1 1-14.
Page 177 - G. McCusker. Games and full abstraction for FPC. In Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 174-183. IEEE Computer Society Press, 1996.
Page 177 - RL Crole and AM Pitts. New foundations for fixpoint computations: Fix-hyperdoctrines and the fix-logic. Information and Computation, 98:171-210, 1992.
Page 176 - HP Barendregt. The lambda calculus, its syntax and semantics. NorthHolland, revised edition, 1984.
Page 184 - G. Winskel. The Formal Semantics of Programming Languages. Foundations of Computing. The MIT Press, Cambridge, Massachusetts, 1993.
