Skip to main content
Springer Nature Link
Log in

Applied Type System

  • Conference paper
Types for Proofs and Programs (TYPES 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3085))

Included in the following conference series:

Abstract

The framework Pure Type System (\(\mathcal{PTS}\)) offers a simple and general approach to designing and formalizing type systems. However, in the presence of dependent types, there often exist some acute problems that make it difficult for \(\mathcal{PTS}\) to accommodate many common realistic programming features such as general recursion, recursive types, effects (e.g., exceptions, references, input/output), etc. In this paper, we propose a new framework Applied Type System (\(\mathcal{ATS}\)) to allow for designing and formalizing type systems that can readily support common realistic programming features. The key salient feature of \(\mathcal{ATS}\) lies in a complete separation between statics, in which types are formed and reasoned about, and dynamics, in which programs are constructed and evaluated. With this separation, it is no longer possible for a program to occur in a type as is otherwise allowed in \(\mathcal{PTS}\). We present not only a formal development of \(\mathcal{ATS}\) but also mention some examples in support of using \(\mathcal{ATS}\) as a framework to form type systems for practical programming.

Partially supported by NSF grants no. CCR-0224244 and no. CCR-0229480

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

') var buybox = document.querySelector("[data-id=id_"+ timestamp +"]").parentNode var buyingOptions = buybox.querySelectorAll(".buying-option") ;[].slice.call(buyingOptions).forEach(initCollapsibles) // springerPlus roll out 10% starts here var springerPlusGroup = setLocalStorageSpringerPlus(); var rollOutSpringerPlus = springerPlusGroup === "B" function setLocalStorageSpringerPlus() { var selectUserKey = "springerPlusRollOut"; var springerPlusGroup = "X"; if (!window.localStorage) return springerPlusGroup; try { var selectUserValue = window.localStorage.getItem(selectUserKey) springerPlusGroup = selectUserValue || randomDistributionSpringerPlus(selectUserKey) } catch (err) { console.log(err) } return springerPlusGroup; } function randomDistributionSpringerPlus(selectUserKey) { var randomGroup = Math.random() < 0.7 ? "A" : "B" window.localStorage.setItem(selectUserKey, randomGroup) return randomGroup } if (rollOutSpringerPlus) { revealSpringerPlus(); } function revealSpringerPlus() { if(buybox) { document.querySelectorAll(".c-springer-plus").forEach(function(node) { node.style.display = "block" }) } } //springerPlus ends here var buyboxMaxSingleColumnWidth = 480 function initCollapsibles(subscription, index) { var toggle = subscription.querySelector(".buying-option-price") subscription.classList.remove("expanded") var form = subscription.querySelector(".buying-option-form") var priceInfo = subscription.querySelector(".price-info") var buyingOption = toggle.parentElement if (toggle && form && priceInfo) { toggle.setAttribute("role", "button") toggle.setAttribute("tabindex", "0") toggle.addEventListener("click", function (event) { var expandedBuyingOptions = buybox.querySelectorAll(".buying-option.expanded") var buyboxWidth = buybox.offsetWidth ;[].slice.call(expandedBuyingOptions).forEach(function(option) { if (buyboxWidth <= buyboxMaxSingleColumnWidth && option != buyingOption) { hideBuyingOption(option) } }) var expanded = toggle.getAttribute("aria-expanded") === "true" || false toggle.setAttribute("aria-expanded", !expanded) form.hidden = expanded if (!expanded) { buyingOption.classList.add("expanded") } else { buyingOption.classList.remove("expanded") } priceInfo.hidden = expanded }, false) } } function hideBuyingOption(buyingOption) { var toggle = buyingOption.querySelector(".buying-option-price") var form = buyingOption.querySelector(".buying-option-form") var priceInfo = buyingOption.querySelector(".price-info") toggle.setAttribute("aria-expanded", false) form.hidden = true buyingOption.classList.remove("expanded") priceInfo.hidden = true } function initKeyControls() { document.addEventListener("keydown", function (event) { if (document.activeElement.classList.contains("buying-option-price") && (event.code === "Space" || event.code === "Enter")) { if (document.activeElement) { event.preventDefault() document.activeElement.click() } } }, false) } function initialStateOpen() { var buyboxWidth = buybox.offsetWidth ;[].slice.call(buybox.querySelectorAll(".buying-option")).forEach(function (option, index) { var toggle = option.querySelector(".buying-option-price") var form = option.querySelector(".buying-option-form") var priceInfo = option.querySelector(".price-info") if (buyboxWidth > buyboxMaxSingleColumnWidth) { toggle.click() } else { if (index === 0) { toggle.click() } else { toggle.setAttribute("aria-expanded", "false") form.hidden = "hidden" priceInfo.hidden = "hidden" } } }) } initialStateOpen() if (window.buyboxInitialised) return window.buyboxInitialised = true initKeyControls() })()

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, pp. 117–441. Clarendon Press, Oxford (1992)

    Google Scholar 

  2. Constable, R.L., Smith, S.F.: Partial objects in constructive type theory. In: Proceedings of Symposium on Logic in Computer Science, Ithaca, New York, June 1987, pp. 183–193 (1987)

    Google Scholar 

  3. Chen, C., Xi, H.: Meta-Programming through Typeful Code Representation. In: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, Uppsala, Sweden, August 2003, pp. 169–180 (2003)

    Google Scholar 

  4. Harper, R.: A simplified account of polymorphic references. Information Processing Letters 51, 201–206 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  5. Honsell, F., Mason, I.A., Smith, S., Talcott, C.: A variable typed logic of effects. Information and Computation 119(1), 55–90 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  6. Hayashi, S., Nakano, H.: PX: A Computational Logic. MIT Press, Cambridge (1988)

    Google Scholar 

  7. Jones, M.P.: Qualified Types: Theory and Practice, November 1994. Cambridge University Press, Cambridge (1994)

    Book  MATH  Google Scholar 

  8. Mendler, N.P.: Recursive types and type constraints in second-order lambda calculus. In: Proceedings of Symposium on Logic in Computer Science, June 1987, pp. 30–36. The Computer Society of the IEEE, Los Alamitos (1987)

    Google Scholar 

  9. Paulin-Mohring, C.: Inductive Definitions in the System Coq: Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  10. Pfenning, F., Paulin-Mohring, C.: Inductively defined types in the Calculus of Constructions. In: Schmidt, D.A., Main, M.G., Melton, A.C., Mislove, M.W. (eds.) MFPS 1989. LNCS, vol. 442, pp. 209–228. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  11. Shao, Z., Saha, B., Trifonov, V., Papaspyrou, N.: A Type System for Certified Binaries. In: Proceedings of 29th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2002), Portland, OR, January 2002, pp. 217–232 (2002)

    Google Scholar 

  12. Xi, H., Chen, C., Chen, G.: Guarded Recursive Datatype Constructors (2002), Available at http://www.cs.bu.edu/~hwxi/GRecTypecon/

  13. Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages, New Orleans, January 2003, pp. 224–235 (2003)

    Google Scholar 

  14. Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, viii+181 pp. pp. viii+189. Available as (1998), http://www.cs.cmu.edu/~hwxi/DML/thesis.ps

  15. Xi, H.: Applied Type System, Available at (July 2003), http://www.cs.bu.edu/~hwxi/ATS/ATS.ps

  16. Xi, H., Pfenning, F.: Dependent Types in Practical Programming. In: Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages, San Antonio, Texas, January 1999, pp. 214–227 (1999)

    Google Scholar 

  17. Zenger, C.: Indexed types. Theoretical Computer Science 187, 147–165 (1997)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Boston University,  

    Hongwei Xi

Authors
  1. Hongwei Xi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, Corso Svizzera 185, 10149, Torino, Italy

    Stefano Berardi

  2. Dipartimento di Informatica, Università di Torino,  

    Mario Coppo

  3. Dipartimento di Informatica, Università di Torino, Corso Svizzera, 185, I-10149, Torino, Italy

    Ferruccio Damiani

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Xi, H. (2004). Applied Type System. In: Berardi, S., Coppo, M., Damiani, F. (eds) Types for Proofs and Programs. TYPES 2003. Lecture Notes in Computer Science, vol 3085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24849-1_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24849-1_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22164-7

  • Online ISBN: 978-3-540-24849-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation