Mechanized Mathematics (and applications)

Papers

• J. Carette and W. M. Farmer A Review of Mathematical Knowledge Management, in Proceedings of MKM 2009, part of Conference on Intelligent Computer Mathematics.
• J. Carette and W. M. Farmer High Level Theories, in Proceedings of Calculemus 2008 (official link).
• J. Carette, W. S. Smith, J. McCutcan, C. K. Anand, and A. Korobkine Case Studies in Model Manipulation for Scientific Computing, in Proceedings of AISC 2008.
• W. S. Smith, J. Carette, and J. McCutchan Commonality Analysis of Families of Physical Models for use in Scientific Computing, in Proceedings of SECSE08 conference
• J. Carette and M. Kucera Partial Evaluation for Maple, (submitted, long version of PEPM paper below)
• J. Carette, O. Kiselyov and C-c. Shan Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages, Proceedings of the 5th ASIAN Symposium on Programming Languages and Systems, 2007. (as well as submitted Journal version).
• Jacques Carette and Oleg Kiselyov Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code(as accepted but unrevised) Science of Computer Programming
• J. Carette, A canonical form for piecewise defined functions in Proceedings of ISSAC 2007.
• J. Carette, W. M. Farmer and V. Sorge A rational reconstruction of a System for Experimental Mathematics, Calculemus 2007.
• J. Carette and M. Kucera Partial Evaluation for Maple, Partial Evaluation and Program Manipulation (PEPM 2007)
• J. Carette and R. Janicki, Computing Properties of Numerical Imperative Programs by Symbolic Computation (accepted) Fundamenta Informaticae (80)
• Wenqin Zhou, J. Carette, D.J. Jeffrey and M.B. Monagan Hierarchical representations with signatures for large expression management, Proceedings of Artificial Intelligence and Symbolic Computation (2006).
• J. Carette, Wenqin Zhou, D.J. Jeffrey and M.B. Monagan Linear Algebra using Maple's LargeExpressions Package, Maple Conference 2006, proceedings published by Maplesoft
• M. Kucera and J. Carette Partial Evaluation and Residual Theorems in Computer Algebra, Calculemus 2006.
• J. Carette and S. Forrest, Mining Maple Code for Contracts, Calculemus 2006.
• W. Kahl, C. Anand, J, Carette Choices in Data Flow for Declarative Assembly, RelMiCS 8 proceedings.
• W. Kahl, J. Carette and X. Ji, Bimonadic Semantics for Basic Pattern Matching Calculi, in Tarmo Uustalu (ed.): Mathematics of Program Construction, MPC 2006, Kuressaare, Estonia, pp. 253--273, LNCS 4014, Springer-Verlag, 2006.
• J. Carette, R. Janicki and Y. Zhai Program Verification by Calculating Relations, Proc. 15th IASTEAD Conf. on Applied Simulation and Modelling, 2006, published by Acta Press.
• J. Carette, and P. Chowdhury Symbolic Interpretation of Legacy Assembly Language, WCRE 2005.
• J. Carette Gaussian Elimination: a case study in efficient genericity with MetaOCaml, Science of Computer Programming, Vol. 62, Num. 1 (September 2005), pages 3-24.
• Jacques Carette and Oleg Kiselyov Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code, GPCE 2005
• Mohamed A. Rabie, Yaser M. Haddara and Jacques Carette A Kinetic Model for the Oxidation of Silicon Germanium Alloys, Journal of Applied Physics, Vol. 98, 2005
• Mohamed A. Rabie, Yaser M. Haddara and Jacques Carette A Comprehensive Kinetic Model for the Wet Oxidation of Silicon Germanium Alloys, Technical Proceedings of the 2005 Nanotechnology Conference, Anaheim, CA, 2005
• S.A. Abramov, J.J. Carette, K.O. Geddes, H.Q. Le: Telescoping in the Context of Symbolic Summation in Maple, Journal of Symbolic Computation, Volume 38, issue 4, pages 1303-1326, October 2004.
• J. Carette Understanding Expression Simplification, in Proceedings of ISSAC 2004, Santander, Spain. slides (pdf)
• J. Carette, W. Farmer, J. Wajs  Trustable Communication between Mathematics Systems in Calculemus 2003 Proceedings, Aracne.

Selected talks

• Invited talk: Modern Mechanized Mathematics given May 20th 2008 at Microsoft Research, Seattle, USA; April 17th 2009 at the IFIP WG 2.11 meeting on program generation, in Mountain View, California; and May 29th 2009 at the SCG/SCL Joint Lab Meeting held in Waterloo, Canada. (latest version of the slides).
• Invited talk: Testing a Computer Algebra System given October 4th 2004 at SQRL, Limerick, Ireland. slides (pdf) and accompanying examples (Maple worksheet).
• Invited talk: Computer Algebra vs Computer Analysis, July 2004, Nijmegen, Netherlands. Introductory slides (pdf) and Live examples of isues (Maple worksheet).
• Talk: A new normal form for Piecewise-defined functions given at MOCAA 2004. slides (pdf).

Technical Reports and preprints

• J. Carette, Alexandre Korobkine, Mark Lawford Automatic and Verifiable Synthesis of Implementations from Mathematical Models
• J. Carette and S. Forrest, Property inference for Maple: an application of Abstract Interpretation, Calculemus 2006.
• C. Anand, J, Carette, W. Kahl, C. Gibbard, R. Lortie Declarative Assembler, SQRL report #20.

Books and Journal issues edited

• Carette, J.; Dixon, L.; Sacerdoti Coen, C.; Watt, S. (Eds.) Intelligent Computer Mathematics, LNAI 5625
• ENTCS Volume 151, Number 1, March 2006 (special issue on Calculemus 2005).
• JAR (special issue on PLMMS 2007 and 2008 -- forthcoming

Iteration of Rational Functions

Theses

• J. Carette: Liens entre la geometrie et la dynamique de ensembles de Julia, Universite de Paris-Sud (Orsay), 1997. Resume/abstract
• J. Carette: Iteration des fractions rationelles, Universite de Montreal, 1991.

Software

• pa_monad