Abstract
Peter Hancock and Anton Setzer developed the notion of interface to introduce interactive programming into dependent type theory. We generalise their notion and get an even simpler definition for interfaces. With this definition the relationship of interfaces to games becomes apparent. In fact from a game theoretical point of view interfaces are nothing other than special games. Programs are strategies for these games. There is an obvious notion of refinement which coincides exactly with the intuition. Interfaces together with the re.nement relation build a complete lattice. We can define several operators on interfaces: tensor, par, choice, bang etc. Every notion has a dual notion by interchanging the viewpoint of player and opponent. Identifying strategies by some kind of behavioural equivalence we conjecture to receive a linear category. All results so far can be achieved in intensional Martin-Löf Type Theory and are verified in the theorem prover Agda (with the exception of associativity of composition which is only proved on paper until now).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Abbott, M., Altenkirch, T., Ghani, N.: Categories of Containers. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 23–38. Springer, Heidelberg (2003)
Abbott, M., Altenkirch, T., Ghani, N., McBride, C.: Derivatives of Containers. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 16–30. Springer, Heidelberg (2003)
Abbott, M., Altenkirch, T., Ghani, N., McBride, C.: \(\partial\) for data. Fundamenta Informatica 65(1-2) (2005)
Abbott, M.G.: Categories of Containers. PhD thesis, University of Leicester (2003)
Abramsky, S.: Semantics of Interaction: an introduction to Game Semantics. In: Dybjer, P., Pitts, A. (eds.) Proceedings of the 1996 CLiCS Summer School, pp. 1–31. Cambridge University Press, Cambridge (1997)
Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Jurdziński, M., Mang, F.Y.C.: Interface Compatibility Checking for Software Modules. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 428–441. Springer, Heidelberg (2002)
Hancock, P., Hyvernat, P.: Programming interfaces and basic topology. In: Proceedings of the second workshop of Formal Topology. Annals of Pure and Applied Logic (2004) (to appear)
Hancock, P., Setzer, A.: Interactive programs in dependent type theory. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 317–331. Springer, Heidelberg (2000)
Hancock, P., Setzer, A.: Specifying interactions with dependent types. In: Workshop on subtyping and dependent types in programming, Portugal, July 7 (2000); Electronic proceedings
Hancock, P., Setzer, A.: Guarded induction and weakly final coalgebras in dependent type theory (extended version). In: Altenkirch, T., Hofmann, M., Hughes, J. (eds.) Dependently typed programming. Dagstuhl Seminar Proceedings 04381, Dagstuhl, Germany (2005)
Hancock, P., Setzer, A.: Interactive programs and weakly final coalgebras in dependent type theory. In: Crosilla, L., Schuster, P. (eds.) From sets and types to topology and analysis: Towards practicable foundations for constructive mathematics. Oxford Logic Guides, pp. 115–136. Oxford University Press, Oxford (2005)
Huet, G.: The zipper. Journal of Functional Programming 7(5), 549–554 (1997)
Hyland, M.: Game Semantics. In: Dybjer, P., Pitts, A. (eds.) Proceedings of the 1996 CLiCS Summer School, pp. 131–184. Cambridge University Press, Cambridge (1997)
Hyvernat, P.: Predicate transformers and linear logic: yet another denotational model. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 115–129. Springer, Heidelberg (2004)
Hyvernat, P.: Synchronous Games, Simulations and λ-calculus. In: Ghica, D.R., McCusker, G. (eds.) Games for Logic and Programming Languages, GaLoP (ETAPS 2005), April 2005, pp. 1–15 (2005)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)
Michelbrink, M.: A generalisation of Hancock-Setzer Interfaces. Draft (2005), Available via, http://www.cs.swan.ac.uk/~csmichel/
Michelbrink, M.: Interfaces as functors, programs as coalgebras - a final coalgebra theorem in intensional type theory (2005) (submitted), Available via, http://www.cs.swan.ac.uk/~csmichel/
Michelbrink, M., Setzer, A.: State-dependent IO-monads in type theory. In: Birkedal, L. (ed.) Proceedings of the 10th Conference on Category Theory in Computer Science (CTCS 2004). Electronic Notes in Theoretical Computer Science, vol. 122, pp. 127–146. Elsevier, Amsterdam (2005)
Sambin, G.: The Basic Picture, a structure for topology (the Basic Picture, I) (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Michelbrink, M. (2006). Interfaces as Games, Programs as Strategies. In: Filliâtre, JC., Paulin-Mohring, C., Werner, B. (eds) Types for Proofs and Programs. TYPES 2004. Lecture Notes in Computer Science, vol 3839. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11617990_14
Download citation
DOI: https://doi.org/10.1007/11617990_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31428-8
Online ISBN: 978-3-540-31429-5
eBook Packages: Computer ScienceComputer Science (R0)