Hostname: page-component-78c5997874-ndw9j Total loading time: 0 Render date: 2024-11-18T00:29:43.870Z Has data issue: false hasContentIssue false
  • English
  • Français

Polarised subtyping for sized types

Published online by Cambridge University Press:  01 October 2008

ANDREAS ABEL
ANDREAS ABEL*
Affiliation:
Department of Computer Science, University of Munich, Oettingenstr. 67, D-80538 München, Germany Email: andreas.abel@ifi.lmu.de
Get access Rights & Permissions [Opens in a new window]

Abstract

We present an algorithm for deciding polarised higher-order subtyping without bounded quantification. Constructors are identified not only modulo β, but also η. We give a direct proof of completeness, without constructing a model or establishing a strong normalisation theorem. Inductive and coinductive types are enriched with a notion of size and the subtyping calculus is extended to account for the inclusions arising between the sized types.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 18 , Special Issue 5: Theory and applications of subtyping , October 2008 , pp. 797 - 822
Copyright
Copyright © Cambridge University Press 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abel, A. (2004) Weak normalisation for the simply-typed lambda-calculus in Twelf. Logical Frameworks and Metalanguages (LFM 2004), IJCAR Satellite Workshop.Google Scholar
Abel, A. and Matthes, R. (2004) Fixed points of type constructors and primitive recursion. In: Marcinkowski, J. and Tarlecki, A. (eds.) Computer Science Logic, 18th Int. Workshop, CSL 2004, 13th Annual Conf. of the EACSL. Springer-Verlag Lecture Notes in Computer Science 3210 190–204.CrossRefGoogle Scholar
Abel, A., Matthes, R. and Uustalu, T. (2005) Iteration schemes for higher-order and nested datatypes. Theoretical Computer Science 333 (1-2)3–66.CrossRefGoogle Scholar
Adams, R. (2005) A Modular Hierarchy of Logical Frameworks, Ph.D. thesis, University of Manchester.CrossRefGoogle Scholar
Altenkirch, T. and Reus, B. (1999) Monadic presentations of lambda terms using generalized inductive types. In: Flum, J. and Rodríguez-Artalejo, M. (eds.) Computer Science Logic, 13th Int. Workshop, CSL '99, 8th Annual Conf. of the EACSL. Springer-Verlag Lecture Notes in Computer Science 1683 453–468.CrossRefGoogle Scholar
Barthe, G., Frade, M. J., Giménez, E., Pinto, L. and Uustalu, T. (2004) Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14 (1)1–45.CrossRefGoogle Scholar
Bird, R. S. and Paterson, R. (1999) De Bruijn notation as a nested datatype. Journal of Functional Programming 9 (1)77–91.CrossRefGoogle Scholar
Compagnoni, A. B. and Goguen, H. (1999) Anti-symmetry of higher-order subtyping. In: Flum, J. and Rodríguez-Artalejo, M. (eds.) Computer Science Logic, 13th Int. Workshop, CSL '99, 8th Annual Conf. of the EACSL. Springer-Verlag Lecture Notes in Computer Science 1683 420–438.CrossRefGoogle Scholar
Compagnoni, A. B. and Goguen, H. (2003) Typed operational semantics for higher-order subtyping. Information and Computing 184 (2)242–297.CrossRefGoogle Scholar
Compagnoni, A. and Goguen, H. (2006) Anti-symmetry of higher-order subtyping and equality by subtyping. Mathematical Structures in Computer Science 16 41–65.CrossRefGoogle Scholar
Coquand, T. (1991) An algorithm for testing conversion in type theory. In: Huet, G. and Plotkin, G. (eds.) Logical Frameworks, Cambridge University Press 255–279.CrossRefGoogle Scholar
Davies, R. and Pfenning, F. (2000) Intersection types and computational effects. Proc. of the 5th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2000) 198–208.CrossRefGoogle Scholar
Duggan, D. and Compagnoni, A. (1999) Subtyping for object type constructors. Presented at FOOL 6.Google Scholar
Girard, J.-Y., Lafont, Y. and Taylor, P. (1989) Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press.Google Scholar
Goguen, H. (1995) Typed operational semantics. In: Deziani-Ciancaglini, M. and Plotkin, G. D. (eds.) Proc. of the 2nd Int. Conf. on Typed Lambda Calculi and Applications, TLCA '95. Springer-Verlag Lecture Notes in Computer Science 902 186–200.CrossRefGoogle Scholar
Goguen, H. (1999) Soundness of the logical framework for its typed operational semantics. In: Girard, J.-Y. (ed.) Proc. of the 4th Int. Conf. on Typed Lambda Calculi and Applications, TLCA'99. Springer-Verlag Lecture Notes in Computer Science 1581.CrossRefGoogle Scholar
Goguen, H. (2005) Justifying algorithms for βη conversion. In: Sassone, V. (ed.) Foundations of Software Science and Computational Structures, FoSSaCS 2005, Edinburgh, UK. Springer-Verlag Lecture Notes in Computer Science 3441 410–424.CrossRefGoogle Scholar
Harper, R. and Pfenning, F. (2005) On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic 6 (1)61–101.CrossRefGoogle Scholar
Hinze, R. (2000) Generalizing generalized tries. Journal of Functional Programming 10 (4)327–351.CrossRefGoogle Scholar
Hughes, J., Pareto, L. and Sabry, A. (1996) Proving the correctness of reactive systems using sized types. Proc. of the 23rd ACM Symp. on Principles of Programming Languages, POPL'96 410–423.CrossRefGoogle Scholar
Joachimski, F. and Matthes, R. (2003) Short proofs of normalization. Archive of Mathematical Logic 42 (1)59–87.CrossRefGoogle Scholar
Mendler, N. P. (1987) Recursive types and type constraints in second-order lambda calculus. Proc. of the 2nd IEEE Symp. on Logic in Computer Science (LICS'87), IEEE Computer Society Press 30–36.Google Scholar
Okasaki, C. (1999) From fast exponentiation to square matrices: An adventure in types. Proc. of the 4th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP '99) 28–35.CrossRefGoogle Scholar
Pierce, B. C. (2002) Types and Programming Languages, MIT Press.Google Scholar
Pierce, B. C. and Steffen, M. (1997) Higher order subtyping. Theoretical Computer Science 176 (1, 2)235–282.CrossRefGoogle Scholar
Steffen, M. (1998) Polarized Higher-Order Subtyping, Ph.D. thesis, Technische Fakultät, Universität Erlangen.Google Scholar
van Raamsdonk, F., Severi, P., Sørensen, M. H. and Xi, H. (1999) Perpetual reductions in lambda calculus. Information and Computing 149 (2)173–225.CrossRefGoogle Scholar
Watkins, K., Cervesato, I., Pfenning, F. and Walker, D. (2003) A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh.CrossRefGoogle Scholar