In my Ph.D., I want to contribute to developing an open archive for formalizations, a common and open infrastructure for managing and sharing formalized mathematical knowledge such as theories, de nitions, and proofs, based on a uniform foundation-independent representation format for libraries, integrate existing formal libraries into this archive and develop methods to e ciently transfer and share information between them.
Theoretically, the main prerequisite has been established in the LATIN project [KMR09]. The LATIN logical framework [Rab13; Cod+11] integrates institutional representations of model theory and type theoretical representations of proof theory and thus permits combining the bene ts of both worlds. A paradigmatic example was published as [HR11]. However, whereas LATIN provides a logical framework, there still remains the problem of integrating the existing formal libraries.
There are two facets of library integration. Firstly, one can refactor a single library to increase reuse through modularity, sharing, and inheritance. Secondly, one can connect or merge two libraries from di erent systems. This requires translating the libraries into a common language (namely MMT) and then identifying and eliminating overlap between the two libraries.
My initial focus will be on integrating the speci cation language PVS [ORS92], with others to follow. PVS is a speci cation language integrated with support tools and a theorem prover under active development at the Computer Science Laboratory of SRI International.
On this basis, I then want to tackle the problem of refactoring and merging libraries. Methodology: The aim is to integrate the syntax, underlying foundation and (ultimately) available libraries of di erent theorem provers into MMT [RK13; HKR12; KRSC11], a uniform foundationindependent representation format for libraries, which allows formalizing the logical foundations alongside the libraries and thus acts as framework for aligning libraries.
Integrating each such library entails four things: 1. Writing an MMT-Plugin, that allows for importing the existing archives into the MMT API, 2. writing an MMT theory, that provides the underlying foundational theory, 3. (potentially) implementing desirable features on the logical framework level (subtyping features, recursive de nition principles etc.) to provide syntactical constructors for the speci c peculiarities of the theorem prover under consideration and 4. (potentially) adapting and improving the MMT language and API in the process.
In the case of PVS, the particular work will be in translating the inductive/coinductive types, record types and the sophisticated subtyping mechanism that PVS provides into the MMT system and to match the conceptually di erent module systems of both languages (PVS uses theories and namespaces quite di erently than MMT).
Furthermore, I investigate methods for refactoring and integrating/connecting the various theorem prover libraries. Useful notions in that regard are alignments [Kal+16] between semantically equivalent symbols across di erent libraries and foundations, interface theories [KRSC11] that abstract from the speci cs of a given foundation and theory intersections [MK15] for generating interface theories.
Preliminary results: Apart from the preliminary results due to others (mentioned in the previous paragraphs), personal results include:
A speci cation of the theorem prover TPS and a translation of its library into MMT (in progress), extensions of the logical framework LF to allow for specifying more complex foundational theories with (among others) judgmental and predicate subtypes, an in nite type hierarchy and record types, including a logical framework based on homotopy type theory as a case study [Mmta], an almost complete speci cation of PVS in MMT using the aforementioned LF extensions [Mmtc], a corresponding translation of PVS's Prelude and NASA libraries into the MMT language [Mmtb], a survey of di erent alignment types and a simple language to specify di erent kinds of alignments [Kal+16], a rst implementation of an expression translation machinery in MMT, that uses alignments and various theory morphisms to translate arbitrary expressions between di erent formal libraries, an implementation of an algorithm for nding alignments between libraries, various improvements on the MMT API (parsing, type checking, new language features, interfaces to external databases and applications).
Future work: I am currently working on survey papers on subtyping principles and type hierarchies { these are intended to serve as a starting point for implementing the corresponding features in MMT as generic as possible.
The PVS speci cation and translation need to be improved with respect to record types, (co)inductive de nition principles and more obscure language features, such as update expressions, to faithfully capture the actual behaviour of the PVS system. Also, I want to additionally import PVS's proof les, to allow for e.g. exporting and translating proof sketches. The latter will require a generic speci cation of various proof tactics.
The expression translation and alignment nding algorithms are in an early stage and need to be improved, evaluated as to their usefulness and extended to allow for more complex translations. Furthermore, I want to investigate methods for generating interface theories from alignments and theory morphisms.
Last but not least, more formal systems will be imported into MMT, providing additional challenges for all the presented research objectives.
N. Bourbaki. \Univers". In: Seminaire de Geometrie Algebrique du Bois Marie - Theorie des topos et cohomologie etale des schemas. Springer, 1964, pp. 185{217.
M. Codescu et al. \Towards Logical Frameworks in the Heterogeneous Tool Set Hets". In: Recent Trends in Algebraic Development Techniques. Ed. by H. Kreowski and T. Mossakowski. LNCS 7137. Springer, 2011.
W. Farmer, J. Guttman, and F. Thayer. \Little Theories". In: Conference on Automated Deduction. Ed. by D. Kapur. 1992, pp. 467{581.
Fulya Horozal, Michael Kohlhase, and Florian Rabe. \Extending MKM Formats at the Statement Level". In: Intelligent Computer Mathematics. Ed. by Johan Jeuring et al. LNAI 7362. Berlin and Heidelberg: Springer Verlag, 2012, pp. 65{80. url: http://kwarc.info/ kohlhase/papers/mkm12-p2s.pdf.
F. Horozal and F. Rabe. \Representing Model Theory in a Type-Theoretical Logical Framework". In: Theoretical Computer Science 412.37 (2011), pp. 4919{4945.
Cezary Kaliszyk et al. \A Standard for Aligning Mathematical Concepts". Submitted to CICM2016. 2016. url: http://kwarc.info/kohlhase/submit/alignments16.pdf. M. Kohlhase, T. Mossakowski, and F. Rabe. The LATIN Project. see https : / / trac . omdoc.org/LATIN/. 2009. [KRSC11] Michael Kohlhase, Florian Rabe, and Claudio Sacerdoti Coen. \A Foundational View on Integration Problems". In: Intelligent Computer Mathematics. Ed. by James Davenport et al. LNAI 6824. Springer Verlag, 2011, pp. 107{122. url: http://kwarc.info/kohlhase/ papers/cicm11-integration.pdf. [Mmta] [Mmtb] [Mmtc] [ORS92] [Rab13] [RK13] [Tea] [HOL]
MathHub MMT/LFX Git Repository. url: http://gl.mathhub.info/MMT/LFX (visited on 05/15/2015).
MathHub PVS/NASA Git Repository. url: http://gl.mathhub.info/PVS/NASA (visited on 05/15/2015).
MathHub PVS/Prelude Git Repository. url: http://gl.mathhub.info/PVS/Prelude (visited on 05/15/2015).
S. Owre, J. Rushby, and N. Shankar. \PVS: A Prototype Veri cation System". In: 11th International Conference on Automated Deduction (CADE). Ed. by D. Kapur. Springer, 1992, pp. 748{752.
F. Rabe. \A Logical Framework Combining Model and Proof Theory". In: Mathematical Structures in Computer Science 23.5 (2013), pp. 945{1001.
Florian Rabe and Michael Kohlhase. \A Scalable Module System". In: Information & Computation 0.230 (2013), pp. 1{54. url: http://kwarc.info/frabe/Research/mmt. pdf.
Coq Development Team. The Coq Proof Assistant: Reference Manual. INRIA. url: https: //coq.inria.fr/refman/.
HOL4 development team. http://hol.sourceforge.net/.