ABSTRACT
We present a generalization of the ideal model for recursive polymorphic types. Types are defined as sets of terms instead of sets of elements of a semantic domain. Our proof of the existence of types (computed by fixpoint of a typing operator) does not rely on metric properties, but on the fact that the identity is the limit of a sequence of projection terms. This establishes a connection with the work of Pitts on relational properties of domains. This also suggests that ideals are better understood as closed sets of terms defined by orthogonality with respect to a set of contexts.
- M. Abadi, B. Pierce, and G. Plotkin. Faithful ideal models for recursive polymorphic types. International Journal of Foundations of Computer Science, 2(1):1--21, Mar. 1991. Summary in Fourth Annual Symposium on Logic in Computer Science, June, 1989.]] Google ScholarDigital Library
- M. Abadi and G. Plotkin. A per model of polymorphism and recursive types. In J. Mitchell, editor, 5th Annual IEEE Symposium on Logic in Computer Science, pages 355--365. IEEE Computer Society Press, 1990.]]Google ScholarCross Ref
- S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1--168. Clarendon Press, 1994.]] Google ScholarDigital Library
- R. Amadio. Recursion over realizability structures. Information and Computation, 91:55--85, 1991.]] Google ScholarDigital Library
- A. W. Appel and D. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems (TOPLAS), 23(5):657--683, 2001.]] Google ScholarDigital Library
- L. Birkedal and R. Harper. Constructing interpretations of recursives types in an operational setting. Information and Computation, 155:3--63, 1999.]] Google ScholarDigital Library
- G. Birkhoff. Lattice theory, volume 25 of Colloquium Publications. American Mathematical Society, 1940.]]Google ScholarCross Ref
- M. Brandt and F. Henglein. Coinductive axiomatization of recursive type equality and subtyping. In R. Hindley, editor, Proc. 3d Int'l Conf. on Typed Lambda Calculi and Applications (TLCA), Nancy, France, April 2-4, 1997, volume 1210 of Lecture Notes in Computer Science (LNCS), pages 63--81. Springer-Verlag, April 1997.]] Google ScholarDigital Library
- K. Bruce and J. Mitchell. PER models of subtyping, recursive types and higher-order polymorphism. In Proc. 19th ACM Symp. on Principles of Programming, pages 316--327, 1992.]] Google ScholarDigital Library
- F. Cardone. Relational semantics for recursive types and bounded quantification. In Proceedings of the Sixteenth International Colloquium on Automata, Languages, and Programming, volume 372 of Lecture Notes in Computer Science, pages 164--178, Stresa, Italy, July 1989. Springer-Verlag.]] Google ScholarDigital Library
- R. Cartwright. Types as intervals. In Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 22--36. ACM Press, 1985.]] Google ScholarDigital Library
- J. Chroboczek. Subtyping recursive games. In Proceedings of the Fifth International Conference on Typed Lambda Calculi and Applications (TLCA'01)., Kraków, Poland, May 2001.]]Google ScholarCross Ref
- L. Dami. Labelled reductions, runtime errors and operational subsumption. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, ICALP, volume 1256 of Lecture Notes in Computer Science, pages 782--793. Springer, 1997.]] Google ScholarDigital Library
- L. Dami. Operational subsumption, an ideal model of subtyping. In A. D. Gordon, A. M. Pitts, and C. Talcott, editors, HOOTS II Second Workshop on Higher-Order Operational Techniques in Semantics, volume 10 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2000.]]Google Scholar
- F. Damm. Subtyping with union types, intersection types and recursive types II. Research Report 2259, INRIA Rennes, May 1994.]]Google Scholar
- V. Danos and J.-L. Krivine. Disjunctive tautologies and synchronisation schemes. In Computer Science Logic'00, volume 1862 of Lecture Notes in Computer Science, pages 292--301. Springer, 2000.]] Google ScholarDigital Library
- R. Davies and F. Pfenning. Intersection types and computational effects. In IC\relax FP '00 {29}, pages 198--208.]] Google ScholarDigital Library
- M. Erné, J. Koslowski, A. Melton, and G. E. Strecker. A primer on Galois connections. In A. R. Todd, editor, Papers on general topology and applications (Madison, WI, 1991), volume 704 of Annals of the New York Academy of Sciences, pages 103--125, New York, 1993. New York Acad. Sci.]]Google Scholar
- M. P. Fiore. A coinduction principle for recursive data types based on bisimulation. Information and Computation, 127(2):186--198, 1996.]]Google ScholarCross Ref
- P. J. Freyd. Algebraically complete categories. In A. Carboni, M. C. Pedicchio, and G. Rosolini, editors, Proceedings of the 1990 Como Category Theory Conference, volume 1488 of Lecture Notes in Mathematics, pages 95--104. Springer--Verlag, 1991.]]Google Scholar
- A. Frisch, G. Castagna, and V. Benzaken. Semantic subtyping. In 17th IEEE Symposium on Logic in Computer Science, pages 137--146. IEEE Computer Society Press, 2002.]] Google ScholarDigital Library
- V. Gapeyev, M. Levin, and B. Pierce. Recursive subtyping revealed. In IC\relax FP '00 {29}. To appear in Journal of Functional Programming.]] Google ScholarDigital Library
- J.-Y. Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301--506, June 2001.]] Google ScholarDigital Library
- A. D. Gordon and A. M. Pitts, editors. Higher Order Operational Techniques in Semantics. Publications of the Newton Institute. Cambridge University Press, 1998.]] Google ScholarDigital Library
- J. Goubault-Larrecq, S. Lasota, and D. Nowak. Logical relations for monadic types. In Proceedings of the 11th Annual Conference of the European Association for Computer Science Logic (CSL'02), volume 2471 of Lecture Notes in Computer Science, pages 553--568. Springer-Verlag, Sept. 2002.]] Google ScholarDigital Library
- H. Hosoya and B. C. Pierce. XDuce: A statically typed XML processing language. ACM Transactions on Internet Technology, 2002. Submitted for publication.]] Google ScholarDigital Library
- H. Hosoya, J. Vouillon, and B. C. Pierce. Regular expression types for XML. ACM Transactions on Programming Languages and Systems (TOPLAS). To appear; short version in ICFP 2000.]] Google ScholarDigital Library
- J. M. E. Hyland. A syntactic characterization of the equality in some models of the λ-calculus. Journal of the London Mathematical Society, 12(2):361--370, 1976.]]Google ScholarCross Ref
- Proceedings of the the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), Montréal, Canada, Sept. 2000. ACM Press.]]Google Scholar
- J.-J. Lévy. An algebraic interpretation of the lambda beta K-calculus; and an application of a labelled lambda-calculus. Theoretical Computer Science, 2(1):97--114, June 1976.]]Google ScholarCross Ref
- D. MacQueen, G. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. Information and Control, 71(1-2):95--130, 1986.]] Google ScholarDigital Library
- I. A. Mason, S. F. Smith, and C. L. Talcott. From operational semantics to domain theory. Information and Computation, 128(1):26--47, 1996.]] Google ScholarDigital Library
- B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991.]]Google Scholar
- A. M. Pitts. Relational properties of domains. Information and Computation, 127:66--90, 1996.]]Google ScholarCross Ref
- A. M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in computer Science, 10:321--359, 2000.]] Google ScholarDigital Library
- A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In Gordon and Pitts {24}, pages 227--273.]]Google Scholar
- S. F. Smith. The coverage of operational semantics. In Gordon and Pitts {39}, pages 307--346.]]Google Scholar
- B. M. R. Stadler and P. F. Stadler. Basic properties of closure spaces, 2002. Supplemental material for {39}.]]Google Scholar
- B. M. R. Stadler and P. F. Stadler. Generalized topological spaces in evolutionary theory and combinatorial chemistry. J. Chem. Inf. Comput. Sci., 42:577--585, 2002. Proceedings MCC 2001, Dubrovnik.]]Google ScholarCross Ref
- I. Stark. Names, equations, relations: practical ways to reason about new. Fundamenta Informaticae, 33(4):369--396, 1998.]] Google ScholarDigital Library
- C. Talcott. Reasoning about functions with effects. In Gordon and Pitts {24}, pages 347--390.]] Google ScholarDigital Library
- C. P. Wadsworth. The relation between computational and denotational properties for Scott's D∞-models of the lambda-calculus. SIAM Journal on Computing, 5(3):488--521, Sept. 1976.]]Google ScholarCross Ref
Index Terms
- Semantic types: a fresh look at the ideal model for types
Recommendations
Semantic types: a fresh look at the ideal model for types
POPL '04We present a generalization of the ideal model for recursive polymorphic types. Types are defined as sets of terms instead of sets of elements of a semantic domain. Our proof of the existence of types (computed by fixpoint of a typing operator) does not ...
System F with coercion constraints
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...
On the power of coercion abstraction
POPL '12Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...
Comments