A Tutorial Implementation of a Dependently Typed Lambda Calculus

• Autorzy: Löh A. , McBride C. , Swierstra W.
• Języki publikacji: EN

Abstrakty

EN

We present the type rules for a dependently typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The article is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe.

Słowa kluczowe

EN

lambda calculus; dependent types

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 102, nr 2
• Strony: 177--207
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Löh A.

autor

McBride C.

autor

Swierstra W.

• Dept. of Information and Computing Sciences, Universiteit Utrecht, P.O. Box 80.089, NL-3508 TB Utrecht, The Netherlands,

Bibliografia

• [1] Abel, A., Altenkirch, T.: A Partial Type Checking Algorithm for Type:Type, International Workshop on Mathematically Structured Functional Programming (V. Capretta, C. McBride, Eds.), 2008.
• [2] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions, Springer Verlag, 2004.
• [3] Coquand, T.: An analysis of Girard's paradox, First IEEE Symposium on Logic in Computer Science, 1986.
• [4] Coquand, T.: An Algorithm for Type-Checking Dependent Types, Science of Computer Programming, 26(1-3), 1996, 167-177.
• [5] Coquand, T., Takeyama, M.: An Implementation of Type: Type, International Workshop on Types for Proofs and Programs, 2000.
• [6] Hinze, R., Löh, A.: lhs2TEX, 2007, http://www.cs.uu.nl/_andres/lhs2tex.
• [7] _5 homepage, 2007, http://www.cs.uu.nl/_andres/LambdaPi.
• [8] Martin-Löf, P.: Intuitionistic type theory, Bibliopolis, 1984.
• [9] McBride, C.: Dependently Typed Functional Programs and their Proofs, Ph.D. Thesis, University of Edinburgh, 1999.
• [10] McBride, C.: Elimination with a Motive, TYPES '00: Selected papers from the International Workshop on Types for Proofs and Programs, Springer-Verlag, 2000.
• [11] McBride, C.: Faking it: Simulating Dependent Types in Haskell, Journal of Functional Programming, 12(5), 2002, 375-392.
• [12] McBride, C.: Epigram: Practical Programming with Dependent Types., Advanced Functional Programming, 2004.
• [13] McBride, C., McKinna, J.: Functional pearl: I am not a number - I am a free variable, Haskell '04: Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, 2004.
• [14] McBride, C., McKinna, J.: The view from the left, Journal of Functional Programming, 14(1), 2004, 69-111.
• [15] McBride, C. et al.: Epigram, 2004, http://www.e-pig.org.
• [16] Meijer, E., Fokkinga, M., Paterson, R.: Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, 5th Conf. on Functional Programming Languages and Computer Architecture, 1991.
• [17] Nordström, B., Petersson, K., Smith, J. M.: Programming in Martin-Löf's Type Theory: An Introduction, Clarendon, 1990.
• [18] Norell, U.: Agda 2, http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php.
• [19] Norell, U.: Towards a practical programming language based on dependent type theory, Ph.D. Thesis, Chalmers University of Technology, 2007.
• [20] Norell, U., Coquand, C.: Type checking in the presence of meta-variables, Submitted to Typed Lambda Calculi and Applications 2007.
• [21] Pierce, B. C.: Types and Programming Languages, MIT Press, Cambridge, MA, USA, 2002, ISBN 0-262-16209-1.
• [22] Pierce, B. C., Turner, D. N.: Local Type Inference, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, 1998, Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1), January 2000, pp. 1-44.
• [23] Pollack, R.: Closure under alpha-conversion, TYPES '93: Proceedings of the international workshop on Types for proofs and programs, 1994.
• [24] Thompson, S.: Type Theory and Functional Programming, Addison Wesley Longman Publishing Co., Inc., 1991.