M. Boespflug, Q. Carbonneaux & O. Hermant (2012):
The λΠ-calculus modulo as a universal proof language.
In: D. Pichardie & T. Weber: Proceedings of PxTP2012: Proof Exchange for Theorem Proving,
pp. 28–43.
(2017):
Intelligent Computer Mathematics.
LNAI.
Springer.
In press.
James Davenport, William Farmer, Florian Rabe & Josef Urban (2011):
Intelligent Computer Mathematics.
LNAI 6824.
Springer Verlag,
doi:10.1007/978-3-642-22673-1.
Paul-Olivier Dehaye, Mihnea Iancu, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Dennis Müller, Markus Pfeiffer, Florian Rabe, Nicolas M. Thiéry & Tom Wiesing (2016):
Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach.
In: Michael Kohlhase, Moa Johansson, Bruce Miller, Leonardo de Moura & Frank Tompa: Intelligent Computer Mathematics 2016,
LNAI 9791.
Springer,
doi:10.1007/978-3-642-39320-4.
Available at https://github.com/OpenDreamKit/OpenDreamKit/blob/master/WP6/CICM2016/published.pdf.
William M. Farmer, Joshua D. Guttman & F. Javier Thayer (1993):
IMPS: An Interactive Mathematical Proof System.
Journal of Automated Reasoning 11(2),
pp. 213–248,
doi:10.1007/BF00881906.
Thibault Gauthier & Cezary Kaliszyk (2014):
Matching concepts across HOL libraries.
In: Stephen Watt, James Davenport, Alan Sexton, Petr Sojka & Josef Urban: CICM,
LNCS 8543.
Springer Verlag,
pp. 267–281,
doi:10.1007/978-3-319-08434-3_20.
Cezary Kaliszyk, Michael Kohlhase, Dennis Müller & Florian Rabe (2016):
Aligning the Libraries of Formal Mathematical Systems.
Available at http://kwarc.info/kohlhase/submit/alignments16.pdf.
Submitted to CPP 2016.
Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase & Florian Rabe (2017):
Classification of Alignments between Concepts of Formal Mathematical Systems.
In: Intelligent Computer Mathematics (CICM) 2017,
doi:10.1007/978-3-540-71067-7_7.
Available at http://kwarc.info/kohlhase/submit/cicm17-alignments.pdf.
In press.
OpenDreamKit Open Digital Research Environment Toolkit for the Advancement of Mathematics.
Available at http://opendreamkit.org.
S. Owre, J. M. Rushby & N. Shankar (1992):
PVS: A Prototype Verification System.
In: D. Kapur: Proceedings of the 11th Conference on Automated Deduction,
LNCS 607.
Springer Verlag,
Saratoga Springs, NY, USA,
pp. 748–752,
doi:10.1007/3-540-55602-8.
Steven Obua & Sebastian Skalberg (2006):
Importing HOL into Isabelle/HOL,
pp. 298–302.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
doi:10.1007/11814771_27.
Florian Rabe (2012):
A Query Language for Formal Mathematical Libraries.
In: Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel & Volker Sorge: Intelligent Computer Mathematics,
LNAI 7362.
Springer Verlag,
pp. 142–157,
doi:10.1007/978-3-642-31374-5_10.
Florian Rabe (2014):
How to Identify, Translate, and Combine Logics?.
Journal of Logic and Computation,
doi:10.1093/logcom/exu079.
Florian Rabe & Michael Kohlhase (2013):
A Scalable Module System.
Information & Computation 0(230),
pp. 1–54.
Available at http://kwarc.info/frabe/Research/mmt.pdf.
A. Trybulec & H. Blair (1985):
Computer Assisted Reasoning with MIZAR.
In: A. Joshi: Proceedings of the 9th International Joint Conference on Artificial Intelligence.
Morgan Kaufmann,
pp. 26–28.
Stephan Watt, James Davenport, Alan Sexton, Petr Sojka & Josef Urban (2014):
Intelligent Computer Mathematics.
LNCS 8543.
Springer,
doi:10.1007/978-3-319-08434-3.