Skip to main content
SpringerLink
Log in

Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus

  • Conference paper
Automated Reasoning (IJCAR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6173))

Included in the following conference series:

Abstract

We introduce a calculus of explicit substitutions for the λ-calculus with linear, affine, and intuitionistic variables and meta-variables. Using a Curry-style formulation, we redesign and extend previously suggested type systems for linear explicit substitutions. This way, we obtain a fine-grained small-step reduction semantics suitable for efficient implementation. We prove that subject reduction, confluence, and termination holds. All theorems have been formally verified in the Twelf proof assistant.

This work was in part supported by NABITT grant 2106-07-0019 of the Danish Strategic Research Council.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416 (1991)

    Article  MathSciNet  Google Scholar 

  2. Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 391–397. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Barras, B.: Programming and computing in hol. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 17–37. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  4. Bierman, G.: On Intuitionistic Linear Logic. PhD thesis, University of Cambridge (1994)

    Google Scholar 

  5. Cervesato, I., de Paiva, V., Ritter, E.: Explicit Substitutions for Linear Logical Frameworks: Preliminary Results. In: Felty, A. (ed.) Workshop on Logical Frameworks and Meta-languages — LFM’99, Paris, France, September 28 (1999)

    Google Scholar 

  6. Chaudhuri, A., Naldurg, P., Rajamani, S.: A type system for data-flow integrity on Windows Vista. SIGPLAN Notices 43(12), 9–20 (2008)

    Article  Google Scholar 

  7. Dowek, G., Hardin, T., Kirchner, C., Pfenning, F.: Unification via explicit substitutions: The case of higher-order patterns. Rapport de Recherche 3591, INRIA, Preliminary version appeared at JICSLP’96 (December 1998)

    Google Scholar 

  8. Gacek, A.: The Abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  9. Ghani, N., de Paiva, V., Ritter, E.: Linear explicit substitutions. Logic Journal of IGPL 8(1), 7 (2000)

    Article  MathSciNet  Google Scholar 

  10. Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 238–252. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Mellies, P.-A.: Typed λ-calculi with explicit substitutions may not terminate. Typed Lambda Calculi and Applications, 328–334 (1995)

    Google Scholar 

  12. Nadathur, G., Mitchell, D.J.: System description: Teyjus - a compiler and abstract machine based implementation of lambda-Prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  13. Nadathur, G., Wilson, D.S.: A notation for lambda terms. a generalization of environment. Theoretical Computer Science 198(1-2), 49–98 (1998)

    Article  MathSciNet  Google Scholar 

  14. Pfenning, F., Schürmann, C.: System description: Twelf — a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  15. Poswolksy, A., Schürmann, C.: Practical programming with higher-order encodings and dependent types. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 93–107. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Schack-Nielsen, A., Schürmann, C.: System description: Celf - a logical framework for deductive and concurrent systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 320–331. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Schack-Nielsen, A., Schürmann, C.: Pattern unification for the lambda calculus with linear and affine types. Under consideration for publication (2010)

    Google Scholar 

  18. Shao, Z., League, C., Monnier, S.: Implementing typed intermediate languages. In: ICFP ’98: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pp. 313–323. ACM, New York (1998)

    Chapter  Google Scholar 

  19. Shinwell, M.R., Pitts, A.M., Gabbay, M.J.: FreshML: Programmming with binders made simple. In: Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pp. 263–274. ACM Press, New York (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IT University of Copenhagen, Copenhagen, Denmark

    Anders Schack-Nielsen & Carsten Schürmann

Authors
  1. Anders Schack-Nielsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carsten Schürmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. RWTH Aachen, LuFG Informatik, 2, Ahornstr. 55, 52074, Aachen, Germany

    Jürgen Giesl

  2. Department of Computer Science, Chalmers University of Technology, 41296, Gothenburg, Sweden

    Reiner Hähnle

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schack-Nielsen, A., Schürmann, C. (2010). Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14203-1_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14202-4

  • Online ISBN: 978-3-642-14203-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation