Programming with proofs and explicit contexts

ABSTRACT

This paper explores a new point in the design space of functional programming: functional programming with dependently-typed higher-order data structures described in the logical framework LF. This allows us to program with proofs as higher-order data. We present a decidable bidirectional type system that distinguishes between dependently-typed data and computations. To support reasoning about open data, our foundation makes contexts explicit. This provides us with a concise characterization of open data, which is crucial to elegantly describe proofs. In addition, we present an operational semantics for this language based on higherorder pattern matching for dependently typed objects. Based on this development, we prove progress and preservation

REFERENCES

• 1: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 2: J. Cheney and R. Hinze. First-class phantom types. Technical Report CUCIS TR2003-1901, Cornell University, 2003.
• 3: Joëlle Despeyroux , Pierre Leleu, Recursion over objects of functional type, Mathematical Structures in Computer Science, v.11 n.4, p.555-572, August 2001 [doi>10.1017/S0960129501003346]
• 4: J. Despeyroux and P. Leleu. Primitive recursion for higher order abstract syntax with dependent types. In International Workshop on Intuitionistic Modal Logics and Applications (IMLA), 1999.
• 5: Joëlle Despeyroux , Frank Pfenning , Carsten Schürmann, Primitive Recursion for Higher-Order Abstract Syntax, Proceedings of the Third International Conference on Typed Lambda Calculi and Applications, p.147-163, April 02-04, 1997
• 6: J. Dunfield and B. Pientka. Case analysis of higher-order data. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08), Electronic Notes in Theoretical Computer Science (ENTCS). Elsevier, June 2008.
• 7: Murdoch Gabbay , Andrew Pitts, A New Approach to Abstract Syntax Involving Binders, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.214, July 02-05, 1999
• 8: Andrew Gacek , Dale Miller , Gopalan Nadathur, Combining Generic Judgments with Recursive Definitions, Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science, p.33-44, June 24-27, 2008 [doi>10.1109/LICS.2008.33]
• 9: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• 10: Daniel R. Licata , Noam Zeilberger , Robert Harper, Focusing on Binding and Computation, Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science, p.241-252, June 24-27, 2008 [doi>10.1109/LICS.2008.48]
• 11: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 12: A. McCreight and C. Schürmann. A meta-linear logical framework. In 4th International Workshop on Logical Frame-works and Meta-Languages (LFM'04), 2004.
• 13: D. Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255--269, Paris, France, June 1991. MIT Press.
• 14: D. Miller. A logic programming language with lambda abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497--536, 1991.
• 15: Aleksandar Nanevski , Frank Pfenning , Brigitte Pientka, Contextual modal type theory, ACM Transactions on Computational Logic (TOCL), v.9 n.3, p.1-49, June 2008 [doi>10.1145/1352582.1352591]
• 16: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 17: F. Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74¿85, Amsterdam, The Netherlands, July 1991.
• 18: Frank Pfenning, Logical frameworks, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 19: Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
• 20: Brigitte Pientka , Frank Pfenning, Tabled higher-order logic programming, Carnegie Mellon University, Pittsburgh, PA, 2003
• 21: Brigitte Pientka, A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 22: B. Pientka and F. Pfenning. Optimizing higher-order pattern unification. In F. Baader, editor, 19th International Conference on Automated Deduction, Miami, USA, Lecture Notes in Artificial Intelligence (LNAI) 2741, pages 473--487. Springer-Verlag, 2003.
• 23: A. Poswolsky and C. Schürmann. Practical programming with higher-order encodings and dependent types. In Proceedings of the 17th European Symposium on Programming (ESOP'08), Mar. 2008.
• 24: C. Schürmann. Automating the Meta Theory of Deductive Systems. PhD thesis, Department of Computer Science, Carnegie Mellon University, 2000. CMU-CS-00-146.
• 25: C. Schürmann, A. Poswolsky, and J. Sarnat. The ∇-calculus. Functional programming with higher-order encodings. In P. Urzyczyn, editor, Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA'05), volume 3461 of Lecture Notes in Computer Science, pages 339--353. Springer, 2005.
• 26: T. Sheard and E. Pasalic. Meta-programming with built-in type equality. In Int'l Workshop on Logical Frameworks and Meta-languages (LFM '04), pages 106--124, 2004.
• 27: Mark R. Shinwell , Andrew M. Pitts , Murdoch J. Gabbay, FreshML: programming with binders made simple, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.263-274, August 25-29, 2003, Uppsala, Sweden
• 28: K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, 2002.
• 29: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

General Terms:
Languages, Theory

Keywords:
dependent types, logical frameworks, type theory