Publications
- Biform Theories: Project description
Abstract
PDF
J. Carette, W. M. Farmer, Yasmine Sharoda
In: F. Rabe,
W. M. Farmer, G. O. Passmore, and A. Youssef,eds.,
Intelligent Computer Mathematics (CICM 2018), Lecture Notes in Computer Science (LNCS), 11006:7686, 2018.
Preprint: arXiv: 1805.02709, 2018.
- HOL Light QE
Abstract
PDF
J. Carette, W. M. Farmer, and P. Laskowski
In: J. Avigad
and A. Mahboubi, eds., Interactive Theorem Proving (ITP 2018), Lecture Notes in Computer Science (LNCS),10895:215234, 2018.
Preprint: arXiv: 1802.00405, 2018.
- Formalizing mathematical knowledge as a biform theory graph: A case study
Abstract
PDF
J. Carette and W. M. Farmer
In: H. Geuvers, M. England,
O. Hasan, F. Rabe, and O. Teschke, eds., Intelligent Computer
Mathematics (CICM 2017), Lecture Notes in Computer Science
(LNCS), 10383:924, 2017 (without appendices).
Preprint with appendices: arXiv: 1704.02253 (43 pp.), 2017.
- Meaning formulas for syntax-based mathematical algorithms
PDF
W. M. Farmer
In: T. Kutsia and A. Voronkov, eds., SCSS 2014 (6th International Symposium on Symbolic
Computation in Software Science), EasyChair Proceedings in
Computing (EPiC), 30:1011, 2014.
Extended Abstract.
- Mechanising mathematics (text interview)
PDF
In: International Innovation North America, May
2013, pp. 2022, Research Media, 2013.
- The formalization of syntax-based mathematical algorithms using quotation and evaluation
Abstract
PDF
W. M. Farmer
In: J. Carette et al., eds., Intelligent
Computer Mathematics (CICM 2013), Lecture Notes in Computer
Science (LNCS), 7961:3550, 2013.
Preprint: arXiv: 1305.6052, 2013.
- Theory Presentation Combinators
PDF
Long version (with proofs)
J. Carette and R. O'Connor
In Proceedings of
Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 7362, 2012.
- MathScheme: Project description
Abstract
PDF
J. Carette, W. M. Farmer, and R. O'Connor
In: J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds.,
Intelligent Computer Mathematics, Lecture Notes in Computer Science (LNCS), 6824:287288, 2011.
- The MathScheme library: Some preliminary experiments
Abstract
PDF
J. Carette, W. M. Farmer, F. Jeremic, V. Maccio, R. O'Connor, and Q. M. Tran
In: A. Asperti, J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, eds.,
Conference on Intelligent Computer Mathematics Work-in-Progress Papers Proceedings,
Technical Report UBLCS-2011-04, pp. 1022, University of Bologna, 2011.
- A review of Mathematical Knowledge Management
Abstract
PDF
J. Carette and W. M. Farmer
In: J. Carette, L. Dixon,
C. Sacerdoti Coen, and S. M. Watt, eds., Intelligent Computer
Mathematics, Lecture Notes in Computer Science (LNCS),
5625:233246, 2009.
- High-level theories
Abstract
PDF
Online
J. Carette and W. M. Farmer
In: S. Autexier, J. Campbell, J. Rubio, V. Sorge, M. Suzuki,
and F. Wiedijk, eds., Intelligent Computer Mathematics, Lecture Notes in
Computer Science (LNCS), 5144:232245, 2008.
- Biform theories in Chiron
Abstract
PostScript
PDF
Online
W. M. Farmer
In: M. Kauers, M. Kerber, R. R. Miner, and
W. Windsteiger, eds., Towards Mechanized Mathematical
Assistants, Lecture Notes in Computer Science (LNCS),
4573:66-79, 2007.
-
A rational reconstruction of a system for experimental
mathematics
Abstract
PostScript
PDF
Online
J. Carette, W. M. Farmer, and V. Sorge
In: M. Kauers,
M. Kerber, R. R. Miner, and W. Windsteiger, eds., Towards
Mechanized Mathematical Assistants, Lecture Notes in Computer
Science (LNCS), 4573:13-26, 2007.
-
A rational reconstruction of a system for experimental
mathematics
J. Carette, W. M. Farmer, and V. Sorge
In: S. Colton,
ed., Proceedings of the Fourteenth Workshop on Automated
Reasoning: Bridging the Gap between Theory and Practice,
Imperial College, London, UK, April 19--20, 2007.
Abstract.
-
Mei A Module System for Mechanized MathematicsSystems
J. Xu
In: J. Carette and F. Wiedijk, eds.,
Proceedings of Programming Languages for Mechanized
Mathematics (PLMMS 2007), 17 pp., Hagenburg, Austria, June
29-30, 2007.
-
Mathematical knowledge management Abstract
W. M. Farmer
In: D. G. Schwartz, ed., Encyclopedia of
Knowledge Management, pp. 599604, Information Science Reference,
2005. Online
Also in: M. E. Jennex, ed., Knowledge Management: Concepts,
Methodologies, Tools and Applications, Chapter 7.3,
pp. 29762983, Information Science Reference, 2007. Online
-
MKM: A new interdisciplinary field of research
Abstract
PostScript
PDF
W. M. Farmer
ACM SIGSAM Bulletin, 38:47-52,
2004.
-
Trustable communication between mathematics systems
Abstract
PostScript
PDF
J. Carette, W. M. Farmer, and J. Wajs
In: T. Hardin and
R. Rioboo, eds., Calculemus 2003 (11th Symposium on the
Integration of Symbolic Computation and Mechanized Reasoning,
Rome, Italy, September 2003), pp. 58-68, Aracne, Rome, Italy,
2003.
This is a shorter, preliminary version of the technical report
below with the same name.
-
An overview of a Formal Framework for Managing
Mathematics Abstract PostScript PDF
W. M. Farmer and M. v. Mohrenschildt
In: B. Buchberger,
G. Gonnet, and M. Hazewinkel, eds., Mathematical Knowledge
Management, special issue of Annals of Mathematics and
Artificial Intelligence, 38:165-191, 2003.
-
A formal framework for managing mathematics
Online
W. M. Farmer and M. v. Mohrenschildt
In: B. Buchberger
and O. Caprotti, eds, Electronic Proceedings of the First
International Workshop on Mathematical Knowledge Management:
MKM 2001, 37 pp., RISC, Hagenburg, Austria, September 24-26,
2001.
Preliminary version of the paper "An overview of a
formal method for managing mathematics".
-
A proposal for the development of an interactive
mathematics laboratory for mathematics education
PostScript
PDF
W. M. Farmer
In: E. Melis, ed., Proceedings of the
Workshop on Deduction Systems for Mathematics Education,
pp. 20-25, CADE-17, Carnegie Mellon University, Pittsburgh,
Pennsylvania, June 16, 2000.
-
Transformers for symbolic computation and formal
deduction
Abstract
PostScript
PDF
W. M. Farmer and M. v. Mohrenschildt
In: S. Colton,
U. Martin and V. Sorge, eds., Proceedings of the Workshop on
the Role of Automated Deduction in Mathematics, pp. 36-45,
CADE-17, Carnegie Mellon University, Pittsburgh, Pennsylvania,
June 20-21, 2000.
-
The Interactive Mathematics Laboratory
Abstract
Online
W. M. Farmer
In: Proceedings of the 31st Annual
Midwest Instruction and Computing Symposium (MICS '98),
pp. 84-94, Fargo, North Dakota and Moorhead, Minnesota, April
16-18, 1998.
Technical Reports
- Frameworks for reasoning about syntax that utilize quotation and evaluation
Abstract
PDF
W. M. Farmer and P. Larjani
McSCert Report 9, 38 pp., McMaster University, 2013 (revised 2014).
Preprint: arXiv: 1308.2149, 2013 (revised 2014).
-
Mei A Module System for Mechanized Mathematics
Systems
PDF
J. Xu
Extended version of Ph.D. Thesis, Technical Report
No. CAS-07-01-WF, 255 pp., McMaster University, 2008.
-
Trustable communication between mathematics systems
Abstract
PostScript
PDF
J. Carette, W. M. Farmer, and J. Wajs
SQRL Report No. 41,
22 pp., McMaster University, 2004.
This is a longer, revised
version of the paper above with the same name.
-
A microkernel for a mechanized mathematics system
Abstract
PostScript
PDF
W. M. Farmer and M. v. Mohrenschildt
Technical Report, 15 pp., McMaster University, 2001.
Selected Talks
-
From structured theories to efficient code in 6 easy steps.
Slides
J. Carette
Invited talk given at joint Lab meeting, March 9, 2012.
-
Mechanized Mathematics.
Slides
J. Carette
Joint PLMMS/Calculemus invited talk given in Paris, France, July 8, 2010.
The slides are inspired by the Takahashi method and only tell part of the story.
-
Logics with underfinedness.
Slides
W. M. Farmer
Tutorial given at CADE-22, McGill University, Montreal, Quebec, Canada, August 2, 2009.
-
Modern Mechanized Mathematics.
Slides
J. Carette
Invited talk given at Microsoft Research, Seattle, USA, May 20, 2008;
At the IFIP WG 2.11 meeting on program generation, in Mountain View, California, USA, April 17, 2009;
Also at the SCG/SCL joint Lab meeting held in Waterloo, Canada, May 29, 2009
IMPS Papers
-
Major IMPS Papers.
-
The IMPS User's Manual (1995).
HTML
PostScript
PDF
-
Full IMPS Bibliography.
HTML
PostScript
PDF
BibTeX