Florian Rabe
Skip Abstract Section
Abstract
Mmt is a framework for designing and implementing formal systems in a way that systematically abstracts from theoretical and practical aspects of their type of theoretical and logical foundations. Thus, definitions, theorems, and algorithms can be stated independently of the foundation, and language designers can focus on the essentials of a particular foundation and inherit a large-scale implementation from Mmt at low cost. Going beyond the similarly motivated approach of meta-logical frameworks, Mmt does not even commit to a particular meta-logic—that makes Mmt level results harder to obtain but also more general.
We present one such result: a type reconstruction algorithm that realizes the foundation-independent aspects generically relative to a set of rules that supply the foundation-specific knowledge. Maybe surprisingly, we see that the former covers most of the algorithm, including the most difficult details. Thus, we can easily instantiate our algorithm with rule sets for several important language features including, e.g., dependent function types. Moreover, our design is modular such that we obtain a type reconstruction algorithm for any combination of these features.
- A. Asperti, C. Sacerdoti Coen, E. Tassi, and S. Zacchiroli. 2006. Crafting a proof assistant. In TYPES, T. Altenkirch and C. McBride (Eds.). Springer, 18--32. Google Scholar
Digital Library
- A. Avron, F. Honsell, I. Mason, and R. Pollack. 1992. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning 9, 3, 309--354. Google ScholarDigital Library
- A. Asperti, W. Ricciotti, C. Sacerdoti Coen, and E. Tassi. 2009. Hints in unification. In Theorem Proving in Higher Order Logics, S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel (Eds.). Springer, 84--98. Google ScholarDigital Library
- A. Asperti, W. Ricciotti, C. Sacerdoti Coen, and E. Tassi. 2012. A bi-directional refinement algorithm for the calculus of (co)inductive constructions. Logical Methods in Computer Science 8, 1.Google ScholarCross Ref
- M. Boespflug, Q. Carbonneaux, and O. Hermant. 2012. The λΠ-calculus modulo as a universal proof language. In Proceedings of PxTP2012: Proof Exchange for Theorem Proving, D. Pichardie and T. Weber (Eds.). 28--43.Google Scholar
- S. Berardi. 1990. Type dependence and Constructive Mathematics. PhD thesis, Dipartimento di Matematica, Università di Torino.Google Scholar
- J. Blanchette, C. Kaliszyk, L. Paulson, and J. Urban. 2016. Hammering towards QED. Journal of Formalized Reasoning 9, 1, 101--148.Google Scholar
- E. Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5, 552--593.Google ScholarCross Ref
- D. Christiansen and E. Brady. 2016. Elaborator reflection: Extending idris in idris. In International Conference on Functional Programming, J. Garrigue, G. Keller, and E. Sumii (Eds.). ACM, 284--297. Google ScholarDigital Library
- D. Cousineau and G. Dowek. 2007. Embedding pure type systems in the lambda-pi-calculus modulo. In Typed Lambda Calculi and Applications, S. Ronchi Della Rocca (Ed.). Springer. 102--117. Google ScholarDigital Library
- Coq Development Team. 2015. The Coq Proof Assistant: Reference Manual. Technical report, INRIA.Google Scholar
- C. Dunchev, F. Guidi, C. Sacerdoti Coen, and E. Tassi. 2015. ELPI: Fast, embeddable, lambda-prolog interpreter. In Logic for Programming, Artificial Intelligence, and Reasoning, M. Davis, A. Fehnker, A. McIver, and A. Voronkov (Eds.). 460--468. Google ScholarDigital Library
- L. de Moura, J. Avigad, S. Kong, and C. Roux. 2015. Elaboration in dependent type theory. Retrieved from https://arxiv.org/abs/1505.04324.Google Scholar
- L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. 2015. The lean theorem prover (system description). In Automated Deduction, A. Felty and A. Middeldorp (Eds.). Springer, 378--388.Google Scholar
- G. Ebner, S. Ullrich, J. Roesch, J. Avigad, and L. de Moura. 2017. A metaprogramming framework for formal verification. Proceedings of the ACM on Programming Languages, 1, ICFP, 34:1--34:29. Google ScholarDigital Library
- F. Ferreira and B. Pientka. 2014. Bidirectional elaboration of dependently typed programs. In Principles and Practice of Declarative Programming, O. Chitil, A. King, and O. Danvy (Eds.). 161--174. Google ScholarDigital Library
- W. Farmer and M. von Mohrenschildt. 2003. An overview of a formal framework for managing mathematics. Annals of Mathematics and Artificial Intelligence 38, 1--3, 165--191. Google ScholarDigital Library
- A. Gacek. 2008. The Abella interactive theorem prover (system description). In Automated Reasoning, A. Armando, P. Baumgartner, and G. Dowek (Eds.). Springer, 154--161. Google ScholarDigital Library
- F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau. 2009. Packaging mathematical structures. In Theorem Proving in Higher Order Logics, S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel (Eds.). Springer, 327--342. Google ScholarDigital Library
- G. Gonthier and A. Mahboubi. 2008. A Small Scale Reflection Extension for the Coq System. Technical Report RR-6455, INRIA.Google Scholar
- R. Harper, F. Honsell, and G. Plotkin. 1993. A framework for defining logics. Journal of the Association for Computing Machinery 40, 1, 143--184. Google ScholarDigital Library
- F. Horozal, M. Kohlhase, and F. Rabe. 2011. Extending OpenMath with sequences. In Intelligent Computer Mathematics, Work-in-Progress Proceedings, A. Asperti, J. Davenport, W. Farmer, F. Rabe, and J. Urban (Eds.). University of Bologna, 58--72.Google Scholar
- F. Honsell, L. Liquori, P. Maksimovic, and I. Scagnetto. 2017. LLFP: A logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. Logical Methods in Computer Science 13, 3.Google Scholar
- R. Harper, D. Sannella, and A. Tarlecki. 1994. Structured presentations and logic representations. Annals of Pure and Applied Logic 67, 113--160.Google ScholarCross Ref
- M. Iancu and F. Rabe. 2012. Management of change in declarative languages. In Intelligent Computer Mathematics, J. Campbell, J. Carette, G. Dos Reis, J. Jeuring, P. Sojka, V. Sorge, and M. Wenzel (Eds.). Springer, 325--340. Google ScholarDigital Library
- M. Kohlhase, T. Mossakowski, and F. Rabe. 2009. The LATIN Project. Retrieved from https://trac.omdoc.org/LATIN/.Google Scholar
- M. Kohlhase and I. Şucan. 2006. A search engine for mathematical formulae. In Artificial Intelligence and Symbolic Computation, T. Ida, J. Calmet, and D. Wang (Eds.). Springer, 241--253. Google ScholarDigital Library
- C. Kaliszyk and J. Urban. 2015. HOL(y)hammer: Online ATP service for HOL light. Mathematics in Computer Science 9, 1, 5--22.Google ScholarCross Ref
- M. Luther. 2001. More on implicit syntax. In Automated Reasoning, R. Goré, A. Leitsch, and T. Nipkow (Eds.). Springer, 386--400. Google ScholarDigital Library
- J. Meng and L. Paulson. 2008. Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning 40, 1, 35--60. Google ScholarDigital Library
- U. Norell. 2005. The Agda WiKi. Retrieved from http://wiki.portal.chalmers.se/agda.Google Scholar
- S. Owre, J. Rushby, and N. Shankar. 1992. PVS: A prototype verification system. In 11th International Conference on Automated Deduction (CADE’92), D. Kapur (Ed.). Springer, 748--752. Google ScholarDigital Library
- L. Paulson. 1994. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer.Google ScholarCross Ref
- B. Pientka and J. Dunfield. 2010. Beluga: A framework for programming and reasoning with deductive systems (system description). In Automated Reasoning, J. Giesl and R. Hähnle (Eds.). Springer, 15--21. Google ScholarDigital Library
- B. Pientka. 2013. An insider’s look at LF type reconstruction: Everything you (n)ever wanted to know. Journal of Functional Programming 23, 1, 1--37. Google ScholarDigital Library
- F. Pfenning and C. Schürmann. 1999. System description: Twelf - a meta-logical framework for deductive systems. In Automated Deduction, H. Ganzinger (Ed.). 202--206. Google ScholarDigital Library
- A. Poswolsky and C. Schürmann. 2008. System description: Delphin - A functional programming language for deductive systems. In International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, A. Abel and C. Urban (Eds.). ENTCS, 135--141.Google Scholar
- F. Rabe. 2012. A query language for formal mathematical libraries. In Intelligent Computer Mathematics, J. Campbell, J. Carette, G. Dos Reis, J. Jeuring, P. Sojka, V. Sorge, and M. Wenzel (Eds.). Springer, 142--157. Google ScholarDigital Library
- F. Rabe. 2013. The MMT API: A generic MKM system. In Intelligent Computer Mathematics, J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger (Eds.). Springer, 339--343. Google ScholarDigital Library
- F. Rabe. 2014. A logic-independent IDE. In Workshop on User Interfaces for Theorem Provers, C. Benzmüller and B. Woltzenlogel Paleo (Eds.). Elsevier, 48--60.Google ScholarCross Ref
- F. Rabe. 2015. Generic literals. In Intelligent Computer Mathematics, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (Eds.). Springer, 102--117. Google ScholarDigital Library
- F. Rabe. 2017. How to identify, translate, and combine logics? Journal of Logic and Computation 27, 6, 1753--1798.Google ScholarCross Ref
- F. Rabe and M. Kohlhase. 2013. A scalable module system. Information and Computation 230, 1, 1--54. Google ScholarDigital Library
- F. Rabe and C. Schürmann. 2009. A practical module system for LF. In Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP’09), J. Cheney and A. Felty (Eds.). ACM Press, 40--48. Google ScholarDigital Library
- M. Wenzel. 1999. Isar - A generic interpretative approach to readable formal proof documents. In Theorem Proving in Higher Order Logics, Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry (Eds.). Springer, 167--184. Google ScholarDigital Library
Index Terms
- A Modular Type Reconstruction Algorithm
Recommendations
Polymorphic algebraic data type reconstruction
PPDP '06: Proceedings of the 8th ACM SIGPLAN international conference on Principles and practice of declarative programmingOne of the disadvantages of statically typed languages is the programming overhead caused by writing all the necessary type information: Both type declarations and type definitions are typically required. Traditional type inference aims at relieving the ...
Bidirectional Elaboration of Dependently Typed Programs
PPDP '14: Proceedings of the 16th International Symposium on Principles and Practice of Declarative ProgrammingDependently typed programming languages allow programmers to express a rich set of invariants and verify them statically via type checking. To make programming with dependent types practical, dependently typed systems provide a compact language for ...
Type checking modular multiple dispatch with parametric polymorphism and multiple inheritance
OOPSLA '11In previous work, we presented rules for defining overloaded functions that ensure type safety under symmetric multiple dispatch in an object-oriented language with multiple inheritance, and we showed how to check these rules without requiring the ...
Comments