A universe of binding and computation

ABSTRACT

We construct a logical framework supporting datatypes that mix binding and computation, implemented as a universe in the dependently typed programming language Agda 2. We represent binding pronominally, using well-scoped de Bruijn indices, so that types can be used to reason about the scoping of variables. We equip our universe with datatype-generic implementations of weakening, substitution, exchange, contraction, and subordination-based strengthening, so that programmers need not reimplement these operations for each individual language they define. In our mixed, pronominal setting, weakening and substitution hold only under some conditions on types, but we show that these conditions can be discharged automatically in many cases. Finally, we program a variety of standard difficult test cases from the literature, such as normalization-by-evaluation for the untyped lambda-calculus, demonstrating that we can express detailed invariants about variable usage in a program's type while still writing clean and clear code.

REFERENCES

• 1: M. Abbott, T. Altenkirch, and N. Ghani. Containers: constructing strictly positive types. Theoretic Computer Science, 342 (1): 3--27, 2005.
• 2: T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In IFIP TC2 Working Conference on Generic Programming, Schloss Dagstuhl, 2003.
• 3: T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types. In CSL 1999: Computer Science Logic. LNCS, Springer-Verlag, 1999.
• 4: S. Ambler, R.L. Crole, and A. Momigliano. Combining higher order abstract syntax with tactical theorem proving and (co)induction. In International Conference on Theorem Proving in Higher-Order Logics, pages 13--30, London, UK, 2002. Springer-Verlag.
• 5: B. Aydemir, A. Charguéraud, B.C. Pierce, R. Pollack, and S. Weirich. Engineering formal metatheory. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 3--15, 2008.
• 6: F. Bellegarde and J. Hook. Substitution: A formal methods case study using monads and transformations. phScience of Computer Programming, 23 (2-3): 287--311, 1994.
• 7: U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In IEEE Symposium on Logic in Computer Science, 1991.
• 8: R.S. Bird and R. Paterson. De Bruijn notation as a nested datatype. Journal of Functional Programming, 9 (1): 77--91, 1999.
• 9: A. Bucalo, M. Hofmann, F. Honsell, M. Miculan, and I. Scagnetto. Consistency of the theory of contexts. phJournal of Functional Programming, 16 (3): 327--395, May 2006.
• 10: V. Capretta and A. Felty. Combining de Bruijn indices and higher-order abstract syntax in Coq. In Proceedings of TYPES 2006, volume 4502 of phLecture Notes in Computer Science, pages 63--77. Springer-Verlag, 2007.
• 11: A. Chlipala. A certified type-preserving compiler from λ-calculus to assembly language. In ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007.
• 12: A. Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In ACM SIGPLAN International Conference on Functional Programming. ACM, 2008.
• 13: K. Crary. Explicit contexts in LF. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2008.
• 14: J. Despeyroux, A. Felty, and A. Hirschowitz. Higher-order abstract syntax in Coq. In M. Dezani-Ciancaglini and G. Plotkin, editors, International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 124--138, Edinburgh, Scotland, 1995. Springer-Verlag.
• 15: M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In IEEE Symposium on Logic in Computer Science, 1999.
• 16: J. Hickey, A. Nogin, X. Yu, and A. Kopylov. Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection. In ACM SIGPLAN International Conference on Functional Programming, pages 172--183, New York, NY, USA, 2006. ACM.
• 17: M. Hofmann. Semantical analysis of higher-order abstract syntax. In IEEE Symposium on Logic in Computer Science, 1999.
• 18: D.R. Licata, N. Zeilberger, and R. Harper. Focusing on binding and computation. In IEEE Symposium on Logic in Computer Science, 2008.
• 19: P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. Rose and J. Shepherdson, editors, Logic Colloquium. Elsevier, 1975.
• 20: C. McBride and J. McKinna. The view from the left. Journal of Functional Programming, 15 (1), 2004.
• 21: D. Miller and A.F. Tiu. A proof theory for generic judgments: An extended abstract. In IEEE Symposium on Logic in Computer Science, pages 118--127, 2003.
• 22: A. Momigliano, A. Martin, and A. Felty. Two-level hybrid: A system for reasoning using higher-order abstract syntax. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007.
• 23: A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. Transactions on Computational Logic, 2007. To appear.
• 24: U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007.
• 25: F. Pfenning and C. Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In H. Ganzinger, editor, International Conference on Automated Deduction, pages 202--206, 1999.
• 26: B. Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 371--382, 2008.
• 27: A.M. Pitts and M.J. Gabbay. A metalanguage for programming with bound names modulo renaming. In R. Backhouse and J.N. Oliveira, editors, Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 230--255. Springer-Verlag, Heidelberg, 2000.
• 28: A. Poswolsky and C. Schürmann. Practical programming with higher-order encodings and dependent types. In European Symposium on Programming, 2008.
• 29: F. Pottier. Static name control for FreshML. In IEEE Symposium on Logic in Computer Science, 2007.
• 30: M.R. Shinwell, A.M. Pitts, and M.J. Gabbay. FreshML: Programming with binders made simple. In ACM SIGPLAN International Conference on Functional Programming, pages 263--274, August 2003.
• 31: R. Virga. phHigher-Order Rewriting with Dependent Types. PhD thesis, Carnegie Mellon University, 1999.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Verification

Keywords:
dependent types, variable binding