Valentin Blot
ABSTRACT
We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains.
The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators.
We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.
- Samson Abramsky and Radha Jagadeesan. 1994. Games and Full Completeness for Multiplicative Linear Logic. Journal of Symbolic Logic 59, 2 (1994), 543--574. Google Scholar
Digital Library
- Samson Abramsky and Radha Jagadeesan. 2005. A game semantics for generic polymorphism. Annals of Pure and Applied Logic 133, 1-3 (2005), 3--37.Google ScholarCross Ref
- Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for PCF. Information and Computation 163, 2 (2000), 409--470. Google ScholarDigital Library
- Samson Abramsky, Radha Jagadeesan, and Matthijs Vákár. 2015. Games for Dependent Types. In 42nd International Colloquium on Automata, Languages, and Programming. Springer, 31--43. Google ScholarDigital Library
- Thorsten Altenkirch, Conor McBride, and James McKinna. 2005. Why dependent types matter. (2005). http://www.e-pig.org/downloads/ydtm.pdf.Google Scholar
- Roberto Amadio and Pierre-Louis Curien. 1998. Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, Vol. 46. Cambridge University Press. Google ScholarDigital Library
- Henk Barendregt. 1992. Lambda Calculi with Types. In Handbook of Logic in Computer Science. Vol. 2. Oxford University Press, 117--309. Google ScholarDigital Library
- Gérard Berry. 1976. Bottom-Up Computation of Recursive Programs. Informatique Théorique et Applications 10, 1 (1976), 47--82.Google Scholar
- Gérard Berry. 1978. Stable Models of Typed lambda-Calculi. In 5th Colloquium on Automata, Languages and Programming. Springer, 72--89. Google ScholarDigital Library
- Gérard Berry and Pierre-Louis Curien. 1982. Sequential Algorithms on Concrete Data Structures. Theoretical Computer Science 20, 3 (1982), 265--321.Google ScholarCross Ref
- Robert Cartwright, Pierre-Louis Curien, and Matthias Felleisen. 1994. Fully Abstract Semantics for Observably Sequential Languages. Information and Computation 111, 2 (1994), 297--401. Google ScholarDigital Library
- Pierre Clairambault. 2009. Least and Greatest Fixpoints in Game Semantics. In 12th International Conference on Foundations Of Software Science And Computational Structures (Lecture Notes in Computer Science). Springer, 16--31.Google Scholar
- Pierre Clairambault and Peter Dybjer. 2014. The biequivalence of locally cartesian closed categories and Martin-Löf type theories. Mathematical Structures in Computer Science 24, 6 (2014).Google Scholar
- Pierre-Louis Curien. 1992. Observable Algorithms on Concrete Data Structures. In 7th Annual Symposium on Logic in Computer Science. IEEE Computer Society, 432--443.Google Scholar
- Peter Dybjer. 1995. Internal Type Theory. In International Workshop on Types for Proofs and Programs, Selected Papers. Springer, 120--134. Google ScholarDigital Library
- Hugo Herbelin. 2005. On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic. In 7th International Conference on Typed Lambda Calculi and Applications (Lecture Notes in Mathematics). Springer, 209--220. Google ScholarDigital Library
- Martin Hofmann and Thomas Streicher. 1998. The Groupoid Interpretation of Type Theory. In Twenty-Five Years of Constructive Type Theory, Proceedings of a Congress held in Venice, October 1995 (Oxford Logic Guides). Oxford University Press, 83--111.Google Scholar
- Martin Hyland and Luke Ong. 2000. On Full Abstraction for PCF: I, II, and III. Information and Computation 163, 2 (2000), 285--408. Google ScholarDigital Library
- Martin Hyland and Andrea Schalk. 2002. Games on Graphs and Sequentially Realizable Functionals. In 17th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 257--264. Google ScholarDigital Library
- Gilles Kahn and Gordon D. Plotkin. 1993. Concrete Domains. Theoretical Computer Science 121, 1&2 (1993), 187--277. Google ScholarDigital Library
- Gilles Kahn and Gordon D. Plotkin. 1993. Concrete Domains. Theoretical Computer Science 121, 1&2 (1993), 187--277. Google ScholarDigital Library
- James Laird. 2013. Game semantics for a polymorphic programming language. journal of the ACM 60, 4 (2013), 29. Google ScholarDigital Library
- Ralph Loader. 2001. Finitary PCF is not decidable. Theoretical Computer Science 266, 1-2 (2001), 341--364. Google ScholarDigital Library
- Per Martin-Löf. 1982. Constructive mathematics and computer programming. In Studies in Logic and the Foundations of Mathematics. Vol. 104. Elsevier, 153--175.Google Scholar
- Per Martin-Löf. 1984. Intuitionistic Type Theory. Bibliopolis.Google Scholar
- Guy McCusker. 1998. Games and full abstraction for a functional metalanguage with recursive types. Springer.Google Scholar
- Erik Palmgren. 1993. An Information System Interpretation of Martin-Löf's Partial Type Theory with Universes. Information and Computation 106, 1 (1993), 26--60. Google ScholarDigital Library
- Erik Palmgren and Viggo Stoltenberg-Hansen. 1990. Domain Interpretations of Martin-Löf's Partial Type Theory. Annals of Pure and Applied Logic 48, 2 (1990), 135--196.Google ScholarCross Ref
- Erik Palmgren and Viggo Stoltenberg-Hansen. 1990. Domain Interpretations of Martin-Löf's Partial Type Theory. Annals of Pure and Applied Logic 48, 2 (1990), 135--196.Google ScholarCross Ref
- Andrew M. Pitts. 1996. Relational Properties of Domains. Information and Computation 127, 2 (1996), 66--90.Google ScholarCross Ref
- Daniele Varacca, Hagen Völzer, and Glynn Winskel. 2004. Probabilistic Event Structures and Domains. In 15th International Conference on Concurrency Theory. Springer, 481--496.Google Scholar
- Glynn Winskel. 1980. Events in computation. Ph.D. Dissertation. University of Edinburgh.Google Scholar
Recommendations
Extensional logic of hyperintensions
Conceptual Modelling and Its Theoretical FoundationsIn this paper I describe an extensional logic of hyperintensions, viz. Tichý's Transparent Intensional Logic (TIL). TIL preserves transparency and compositionality in all kinds of context, and validates quantifying into all contexts, including ...
Extensional Higher-Order Paramodulation in Leo-III
AbstractLeo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with ...
Extensional Equality in Intensional Type Theory
LICS '99: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer ScienceWe present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant ...
Comments