“An Integrated Framework For Computer Algebra
And Computer Theorem Proving”

Publications

  1. 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:76–86, 2018. Preprint: arXiv: 1805.02709, 2018.


  2. 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:215–234, 2018. Preprint: arXiv: 1802.00405, 2018.


  3. 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:9–24, 2017 (without appendices). Preprint with appendices: arXiv: 1704.02253 (43 pp.), 2017.


  4. 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:10–11, 2014.
    Extended Abstract.


  5. Mechanising mathematics (text interview) PDF
    In: International Innovation North America, May 2013, pp. 20–22, Research Media, 2013.


  6. 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:35–50, 2013. Preprint: arXiv: 1305.6052, 2013.


  7. 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.


  8. 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:287–288, 2011.


  9. 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. 10–22, University of Bologna, 2011.


  10. 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:233–246, 2009.


  11. 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:232–245, 2008.


  12. 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.


  13. 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.


  14. 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.

  15. 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.


  16. Mathematical knowledge management Abstract
    W. M. Farmer
    In: D. G. Schwartz, ed., Encyclopedia of Knowledge Management, pp. 599–604, Information Science Reference, 2005. Online
    Also in: M. E. Jennex, ed., Knowledge Management: Concepts, Methodologies, Tools and Applications, Chapter 7.3, pp. 2976–2983, Information Science Reference, 2007. Online


  17. MKM: A new interdisciplinary field of research Abstract PostScript PDF
    W. M. Farmer
    ACM SIGSAM Bulletin, 38:47-52, 2004.


  18. 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.


  19. 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.


  20. 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".


  21. 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.


  22. 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.


  23. 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

  1. 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).


  2. 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.


  3. 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.


  4. 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

  1. From structured theories to efficient code in 6 easy steps. Slides
    J. Carette
    Invited talk given at joint Lab meeting, March 9, 2012.


  2. 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.


  3. Logics with underfinedness. Slides
    W. M. Farmer
    Tutorial given at CADE-22, McGill University, Montreal, Quebec, Canada, August 2, 2009.


  4. 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

  1. Major IMPS Papers.


  2. The IMPS User's Manual (1995). HTML PostScript PDF


  3. Full IMPS Bibliography. HTML PostScript PDF BibTeX