Contextual modal type theory

ABSTRACT

The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this article we investigate the consequences of relativizing these concepts to explicitly specified contexts. We obtain contextual modal logic and its type-theoretic analogue. Contextual modal type theory provides an elegant, uniform foundation for understanding metavariables and explicit substitutions. We sketch some applications in functional programming and logical frameworks.

REFERENCES

• 1: M. Abadi , L. Cardelli , P.-L. Curien , J.-J. Levy, Explicit substitutions, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.31-46, December 1989, San Francisco, California, United States [doi>10.1145/96709.96712]
• 2: Natasha Alechina , Michael Mendler , Valeria de Paiva , Eike Ritter, Categorical and Kripke Semantics for Constructive S4 Modal Logic, Proceedings of the 15th International Workshop on Computer Science Logic, p.292-307, September 10-13, 2001
• 3: Attardi, G. and Simi, M. 1994. Proofs in context. In Principles of Knowledge Representation and Reasoning, J. Doyle, E. Sandewall, and P. Torasso, Eds. Morgan Kaufman, San Francisco, CA, 16--26.
• 4: Attardi, G. and Simi, M. 1995. A formalization of viewpoints. Fundamenta Informaticae 23, 3, 149--173.
• 5: Nikolaj Bjørner , César Muñoz, Absolute Explicit Unification, Proceedings of the 11th International Conference on Rewriting Techniques and Applications, p.31-46, July 10-12, 2000
• 6: Mirna Bognar , Roel De Vrijer, A Calculus of Lambda Calculus Contexts, Journal of Automated Reasoning, v.27 n.1, p.29-59, July 2001 [doi>10.1023/A:1010654904735]
• 7: Buvač, S. 1996. Quantificational logic of context. In Proceedings of the Thirteenth National Conference on Artificial Intelligence. 600--606.
• 8: Buvač, S., Buvač, V., and Mason, I. 1995. Metamathematics of contexts. Fundamenta Informaticae 23, 3, 412--419.
• 9: Calcagno, C., Moggi, E., and Taha, W. 2004. ML-like inference for classifiers. In European Symposium on Programming, ESOP'04, D. Schmidt, Ed. Lecture Notes in Computer Science, 2986. Springer-Verlag, Berlin, Germany, 79--93.
• 10: Cartmell, J. 1986. Generalized algebraic theories and contextual categories. Ann. Pure Appl. Log. 32, 209--243.
• 11: Iliano Cervesato , Frank Pfenning, A linear logical framework, Information and Computation, v.179 n.1, p.19-75, November 25, 2002 [doi>10.1006/inco.2001.2951]
• 12: Laurent Dami, A lambda-calculus for dynamic binding, Theoretical Computer Science, v.192 n.2, p.201-231, Feb. 20, 1998 [doi>10.1016/S0304-3975(97)00150-3]
• 13: R. Davies, A temporal-logic approach to binding-time analysis, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.184, July 27-30, 1996
• 14: Rowan Davies , Frank Pfenning, A modal analysis of staged computation, Journal of the ACM (JACM), v.48 n.3, p.555-604, May 2001 [doi>10.1145/382780.382785]
• 15: de Groote, P. 2002. On the strong normalisation of intuitionistic natural deduction with permutation-conversions. Inform. Computat. 178, 2 (Nov.), 441--464.
• 16: de Paiva, V. 2003. Natural deduction and context as (constructive) modality. In Modelling and Using Context, P. Blackburn, C. Ghidini, R. M. Turner, and F. Giunchiglia, Eds. Lecture Notes in Artificial Inteligence, vol. 2680. Springer, Berlin, Germany, 116--129.
• 17: Gilles Dowek , Therese Hardin , Claude Kirchner, Higher-order Unification via Explicit Substitutions, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.366, June 26-29, 1995
• 18: Gilles Dowek , Therese Hardin , Claude Kirchner, Higher-order Unification via Explicit Substitutions, Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, p.366, June 26-29, 1995
• 19: Herman Geuvers , Gueorgui I. Jojgov, Open Proofs and Open Terms: A Basis for Interactive Logic, Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, p.537-552, September 22-25, 2002
• 20: Giunchiglia, F. 1993. Contextual reasoning. Epistemologica 16, 345--364.
• 21: Fausto Giunchiglia , Luciano Serafini, Multilanguage hierarchical logics, or: how we can do without modal logics, Artificial Intelligence, v.65 n.1, p.29-70, Jan. 1994 [doi>10.1016/0004-3702(94)90037-X]
• 22: 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]
• 23: Masatomo Hashimoto , Atsushi Ohori, A typed context calculus, Theoretical Computer Science, v.266 n.1-2, p.249-272, 09/06/2001 [doi>10.1016/S0304-3975(00)00174-2]
• 24: Joshua S. Hodas , Dale Miller, Logic programming in a fragment of intuitionistic linear logic, Information and Computation, v.110 n.2, p.327-365, May 1, 1994
• 25: Jojgov, G. I. 2003. Holes with binding power. In Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, H. Geuvers and F. Wiedijk, Eds. Lecture Notes in Computer Science, vol. 2646. Springer, Berlin, Germany, 162--181.
• 26: Kripke, S. 1959. A completeness theorem in modal logic. J. Symbol. Log. 24, 1--14.
• 27: Shinn-Der Lee , Daniel P. Friedman, Enriching the lambda calculus with contexts: toward a theory of incremental program construction, Proceedings of the first ACM SIGPLAN international conference on Functional programming, p.239-250, May 24-26, 1996, Philadelphia, Pennsylvania, United States
• 28: Chuck Liang , Gopalan Nadathur, Tradeoffs in the Intensional Representation of Lambda Terms, Proceedings of the 13th International Conference on Rewriting Techniques and Applications, p.192-206, July 22-24, 2002
• 29: Magnusson, L. 1995. The implementation of ALF—a proof editor based on Martin-Löf's monomorphic type theory with explicit substitutions. Ph.D. dissertation. Chalmers University of Technology and Göteborg University, Göteborg, Sweden.
• 30: Martin-Löf, P. 1996. On the meanings of the logical constants and the justifications of the logical laws. Nordic J. Philosoph. Log. 1, 1, 11--60.
• 31: Ian A. Mason, Computing with Contexts, Higher-Order and Symbolic Computation, v.12 n.2, p.171-201, September 1999 [doi>10.1023/A:1010052222987]
• 32: John McCarthy, Generality in artificial intelligence, Communications of the ACM, v.30 n.12, p.1030-1035, Dec. 1987 [doi>10.1145/33447.33448]
• 33: McCarthy, J. 1993. Notes on formalizing contexts. In Proceedings of the International Joint Conference on Artificial Intelligence (Chambery, France). 555--560.
• 34: Miller, D. 1991. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Computat. 1, 4, 497--536.
• 35: Montague, R. 1963. Syntactical treatment of modalities, with corollaries on reflexion principles and finite axiomatizability. Acta Philosophica Fennica 16, 153--167.
• 36: Moody, J. 2003. Modal logic as a basis for distributed computation. Tech. rep. CMU-CS-03-194. Carnegie Mellon University, Pittsburgh, PA.
• 37: César Muñoz, Dependent types and explicit substitutions: a meta-theoretical development, Mathematical Structures in Computer Science, v.11 n.1, p.91-129, February 2001 [doi>10.1017/S0960129500003261]
• 38: Tom Murphy VII , Karl Crary , Robert Harper , Frank Pfenning, A Symmetric Modal Lambda Calculus for Distributed Computing, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.286-295, July 13-17, 2004 [doi>10.1109/LICS.2004.7]
• 39: Aleksandar Nanevski, From dynamic binding to state via modal possibility, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.207-218, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888271]
• 40: Aleksandar Nanevski , Frank Pfenning, Functional programming with names and necessity, Carnegie Mellon University, Pittsburgh, PA, 2004
• 41: Aleksandar Nanevski , Frank Pfenning, Staged computation with names and necessity, Journal of Functional Programming, v.15 n.6, p.893-939, November 2005 [doi>10.1017/S095679680500568X]
• 42: Aleksandar Nanevski , Brigitte Pientka , Frank Pfenning, A modal foundation for meta-variables, Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.1-6, August 26, 2003, Uppsala, Sweden [doi>10.1145/976571.976582]
• 43: Frank Pfenning, Structural cut elimination, Information and Computation, v.157 n.1-2, p.84-141, Feb. 25/March 15, 2000 [doi>10.1006/inco.1999.2832]
• 44: Frank Pfenning, Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.221, June 16-19, 2001
• 45: Frank Pfenning , Rowan Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, v.11 n.4, p.511-540, August 2001 [doi>10.1017/S0960129501003322]
• 46: 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
• 47: Brigitte Pientka , Frank Pfenning, Tabled higher-order logic programming, Carnegie Mellon University, Pittsburgh, PA, 2003
• 48: Pientka, B. and Pfennning, F. 2003. Optimizing higher-order pattern unification. In International Conference on Automated Deduction, CADE'03, F. Baader, Ed. Lecture Notes in Computer Science, vol. 2741. Springer, Berlin, Germany, 473--487.
• 49: Masahiko Sato , Takafumi Sakurai , Rod Burstall, Explicit Environments, Fundamenta Informaticae, v.45 n.1-2, p.79-115, January 2001
• 50: Sato, M., Sakurai, T., and Kameyama, Y. 2002. A simply typed context calculus with first-class environments. J. Funct. Log. Programm. 2002, 4 (Mar.).
• 51: Sato, M., Sakurai, T., Kameyama, Y., and Igarashi, A. 2003. Calculi of meta-variables. In International Workshop on Computer Science Logic, CSL'03, M. Baaz and J. A. Makowsky, Eds. Lecture Notes in Computer Science, vol. 2803. Springer, Berlin, Germany, 484--497.
• 52: Schürmann, C., Poswolsky, A., and Sarnat, J. 2005. The ∇-calculus: Functional programming with higher-order encodings. In International Conference on Typed Lambda Calculus and Applications, TLCA'05, P. Urzyczyn, Ed. Lecture Notes in Computer Science, vol. 3461. Springer, Berlin, Germany, 339--353.
• 53: Luciano Serafini , Paolo Bouquet, Comparing formal theories of context in AI, Artificial Intelligence, v.155 n.1-2, p.41-67, May 2004 [doi>10.1016/j.artint.2003.11.001]
• 54: Luciano Serafini , Fausto Giunchiglia, ML Systems: A Proof Theory for Contexts, Journal of Logic, Language and Information, v.11 n.4, p.471-518, Fall 2002 [doi>10.1023/A:1019967901393]
• 55: Simpson, A. K. 1994. The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh.
• 56: Strecker, M. 1999. Construction and deduction in type theories. Ph.D. dissertation. Universität Ulm, Ulm, Germany.
• 57: Walid Taha , Michael Florentin Nielsen, Environment classifiers, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-37, January 15-17, 2003, New Orleans, Louisiana, USA
• 58: Walid Taha , Tim Sheard, Multi-stage programming with explicit annotations, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.203-217, June 12-13, 1997, Amsterdam, The Netherlands
• 59: Richmond H. Thomason, Type Theoretic Foundations for Context, Part 1: Contexts as Complex Type-Theoretic Objects, Proceedings of the Second International and Interdisciplinary Conference on Modeling and Using Context, p.351-360, September 01, 1999
• 60: Thomason, R. H. 2003. Dynamic contextual intensional logic: Logical foundations and an application. In Modeling and Using Context, P. Blackburn, C. Ghidini, R. M. Turner, and F. Giunchiglia, Eds. Lecture Notes in Artificial Inteligence, vol. 2680. Springer, Berlin, Germany, 328--341.
• 61: Watkins, K., Cervesato, I., Pfenning, F., and Walker, D. 2002. A concurrent logical framework I: Judgments and properties. Tech. rep. CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA. Revised May 2003.
• 62: Weyhrauch, R. W. 1979. Prolegomena to a theory of mechanized formal reasoning. Artific. Intell. 13, 1--2, 133--170.
• 63: Philip Wickline , Peter Lee , Frank Pfenning, Run-time code generation and modal-ML, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.224-235, June 17-19, 1998, Montreal, Quebec, Canada
• 64: Philip Wickline , Peter Lee , Frank Pfenning , Rowan Davies, Modal types as staging specifications for run-time code generation, ACM Computing Surveys (CSUR), v.30 n.3es, Sept. 1998 [doi>10.1145/289121.289129]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Modal logic

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Frameworks

General Terms:
Design, Theory

Keywords:
Type theory, intuitionistic modal logic, logical frameworks