Software
Talks
Books/Proceedings edited
Theses.
Research Papers
- S. Smith, P. Michalski, J. Carette, Z. Keshavarz-Motamed
State of the Practice for Lattice Boltzmann Method Software,
Archives of Computations Methods in Engineering
(DOI).
- J. Carette, W. S. Smith, J. Balaci
Generating Software for Well-Understood Domains,
in Proceedings of EVCS 2023.
There is also a
version on arXiv.
- C. Lengauer and J. Carette
Eelco Visser as a Founding Member of the IFIP WG 2.11,
in Proceedings of EVCS 2023.
- J Carette, G Ortiz, A Sabry
Symbolic Execution of Hadamard-Toffoli Quantum Circuits.
Proc. of PEPM 2023.
There is also a github repository with all the code. And slides
- G.M.Smith and J. Carette
What Lies Beneath - A Survey of Affective Theory Use in Computational Models of Emotion
published in IEEE Transactions on Affective Computing, Vol 13
issue 4. official version.
- W. de Meo, J. Carette.
A Machine-checked Proof of Birkhoff's Variety Theorem in Martin-Loef Type Theory.
27th International Conference on Types for Proofs and Programs (TYPES 2021)
LIPIcs volume 239. p. 4:1-4:21. Published 2022.
DOI: 10.4230/LIPIcs.TYPES.2021.4.
publisher version.
- J Carette, WM Farmer, Y Sharoda
Leveraging the Information Contained in Theory Presentations
(also: local version and
official link),
Proceedings of CICM 2020. LNCS 12236, p.55-70.
- Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe
Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal,
Mathematical Intelligencer, Vol 42, pages 78-87.
- J. Carette, S. Soraine
Types for Players,
in PLIE 2021 (Programming Languages in Entertainment), part of AIIDE-21.
Volume 3217 of CEUR-WS.
- J Carette, RP James, A Sabry
Embracing the Laws of Physics: Three Reversible Models of Computation,
also available from arxiv;
published in Advances in Computers; beware, the publisher's version is
super ugly as it was done in Word. I recommend using our preprint.
- Jason Z.S. Hu, Jacques Carette
Formalizing Category Theory in Agda
in Proc. of CPP 2021. This is the proper version of what was
previously called
Proof-Relevant Category Theory in Agda (on arxiv).
- J Carette, B. MacLachlan, S Smith
GOOL: Generic Object-Oriented Language Short version, as it will appear in Proc. of PEPM 2020.
There is a Long version on arxiv; a local version is also available.
- M. Al-hassy, J Carette, W Kahl
A Language Feature to Unbundle Data at Will (short paper)
Proc. of GPCE 2019.
- R Walia, P Narayanen, J Carette, C Shan, S Tobin-Hochstadt
From High-Level Inference Algorithms to Efficient Code,
Proc. of ACM Program. Lang., Vol 3, No. ICFP, August 2019.
DOI:10.1145/3341702
- S. Soraine, J. Carette
Towards Accessibility of Games: Mechanical Experience, Competence Profiles and Jutsus.
Journal of Games, Self & Society 2 (1), p.150-209. 2020. There's also a
full version
with extra material (11 mores pages) in an appendix.
- G. Smith, J. Carette
Design Foundations for Emotional Characters, author's copy,
Eludamos, Journal for Computer Game Culture 10 (1), p.109-140.
Publisher's version.
- J Carette, WM Farmer
arxiv:
Towards Specifying Symbolic Computation,
(local copy), in
Proceedings of CICM 2019. LNCS 11617, p.109-124.
official Springer link.
- C Hutslar, J Carette, A Sabry
A Library of Reversible Circuit Transformations (Work in Progress),
published in the proceedings of the International Conference on
Reversible Computation, RC 2018. p. 339--345, LNCS 11106.
- M Peacocke, RJ Teather, J Carette, IS MacKenzie, V McArthur
An empirical comparison of first-person shooter information displays: HUDS, diegetic displays, and spatial representations (preprint),
official version (behind paywall), but
also a local copy (as per funding mandates),
in Entertainment Computing vol 26, p. 41-58. (2018)
- J Carette, WM Farmer, Y Sharoda
Biform Theories: Project Description,
(official link),
in Proceedings of CICM 2018 (LNCS 11006), p. 76-86.
- J Carette, WM Farmer, P Laskowski
HOL Light QE,
in Proceedings of Interactive Theorem Proving 2018, part of FLOC 2018.
- WS Smith, Z Zeng, J Carette
Seismology software: state of the practice,
in Journal of Seismology, Vol 22 no 3, p. 755-788.
- J Carette, CH Chen, V Choudhury, A Sabry
From Reversible Programs to Univalent Universes and Back (arxiv link),
official version,
in Proceedings of Mathematical Foundations of Programming Semantics (MFPS XXXIII),
ENTCS Vol. 336, (April 2018), p. 5 -25.
- J Carette, WM Farmer
Formalizing mathematical knowledge as a biform theory graph: A case study,
in Proceedings of CICM 2017, p. 9-24.
- WS Smith, DA Lazzarato, J Carette
State of the practice for mesh generation and mesh processing software,
in Advances in Engineering Software vol 100, p. 53-71.
- D Szymczak, S Smith, J Carette
Position paper: A knowledge-based approach to scientific software development,
in Proceedings of 2016 IEEE/ACM International Workshop on Software
Engineering for Science (SE4Science), p. 23-26.
- J Carette, A Sabry
Computing with semirings and weak rig groupoids,
in Proceedings of ESOP 2016, p. 123-148.
- P. Narayanan, J. Carette, W. Romano, CS Shan, R. Zinkov
Probabilistic Inference by Program Transformation in Hakaru (System Description),
in Proceedings of Functional and Logic Programming, LNCS 9613.
- J. Carette, C.-c. Shan
Simplifying probabilistic programs using Computer Algebra,
in Proceedings of PADL 2016. LNCS 9585, p.135-152.
- M Peacocke, RJ Teather, J Carette, IS MacKenzie
Evaluating the effectiveness of HUDs and diegetic ammo displays in first-person shooter games
in Proceedings of IEEE GEM 2015 conference.
- RJ Teather, J Carette, M Thevathasan
Uniform vs non-uniform scaling of shooter games on large displays
in Proceedings of IEEE GEM 2015 conference.
- Geneva Smith, Robert J Teather, Jordan Lass, Jacques Carette
Effects of interior bezel size and configuration on gaming performance with large tiled displays in
Proceedings of IEEE GEM 2015 conference, p. 1-8.
- Geneva Smith, Robert J Teather, Jordan Lass, Jacques Carette
Effects of Bezel Size in Large Tiled Display Gaming in
in Proceedings of the 3rd ACM Symposium on Spatial User Interaction (2015), p. 129-129
- G Browning, RJ Teather, J Carette
Differences in Perspective and Software Scaling
in Proceedings of the 3rd ACM Symposium on Spatial User Interaction (2015), p. 128-128
- J. Carette, W.M. Farmer and M. Kohlhase,
Realms: A structure for consolidating knowledge about mathematical theories, in Proceedings of CICM 2014, LNCS 8543, p. 252-266.
- M. Peacocke, R.J. Teather, J. Carette,
Diagetic vs. non-diagetic game displays,
IEEE GEM 2014 Proceedings, p. 1-2. (Extended Abstract)
- R.J. Teather, M. Thevathasan, J. Carette,
Scale Effects in "Bullet Hell" Games in
IEEE GEM 2014 Proceedings, p. 303-304. (Extended Abstract)
- J. Carette, R. O'Connor
Theory Presentation Combinators,
in Proceedings of CICM 2012, LNCS 7362. See also
long version (with proofs).
- J. Carette, A. Stump,
Towards Typing for Small-Step Direct Reflection,
in Proceedings of PEPM 2012, p. 93-96, ACM 2012.
- Feng, Xin and Marr, Simon and O'Callaghan, Tony and Zhou, Zhi Quan and Carette, Jacques,
Function substitution: Towards constraint solving in software testing
in Proceedings of 2012 IEEE International Conference on Quality Software (QSIC),
p. 31-40.
- J. Carette, W.M. Farmer, R. O'Connor
MathScheme: Project Description
in Proceedings of CICM 2011,
LNCS 6824, p. 287--288.
- J. Carette, W.M. Farmer, F. Jeremic, V. Maccio, R. O'Connor,
Q.M. Tran The MathScheme Library: Some Preliminary Experiments,
in Work-in-Progress Proceedings for CICM 2011, Tech. Report UVLCS-2011-04,
University of Bologna, Italy. p. 10-22.
- L. Beyak, J. Carette
SAGA: A DSL for Story Management,
in Proceedings of DSL 2011,
EPTCS vol. 66, p. 48-67.
- J. Carette, M. Elsheik, S. Smith.
Generative Geometric Kernel, in Proceedings of PEPM 2011. ACM, p.53-62.
- J. Carette, Alan P. Sexton, Volker Sorge, and Stephen M. Watt.
Symbolic Domain Decomposition, in Proceedings of Calculemus 2010, part of CICM 2010.
- J. Carette, O. Kiselyov and C-c. Shan
Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages Journal of Functional Programming 19(5):509-543, 2009.
- James H. Davenport, J. Carette, Sparsity Challenges,
in Proceedings of SYNASC 2009 (official link)
- 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. McCutchan, 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. (Superceded by journal version above).
- 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, 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
Gaussian Elimination: a case study in efficient genericity with MetaOCaml, Science of Computer Programming,
Vol. 62, Num. 1 (September 2006), pages 3-24.
- 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.
- W. Kahl, C. Anand, J, Carette
Control-Flow Semantics for Assembly-Level-Data-Flow Graphs,
RelMiCS 8 proceedings. (2005)
- J. Carette, and P. Chowdhury
Symbolic Interpretation of Legacy Assembly Language, WCRE 2005.
- 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.
Software
Various pieces of software that I have co-authored:
You can also find some work-in-progress, experimental code such as
- Theories and Data-Structures
wherein we attempt to show that some mathematical theories and some (functional) data-structures
are inextricably linked.
I have also contributed some code to
Selected talks
- Invited talk at CICM 2024 in Montreal,
Learning from 'Invisible Mathematics'
- Slides for Definite Folds,
presentend at SPLS 2022 in Stirling (Scotland).
- slides for Symbolic Execution of Hadamard-Toffoli Quantum Circuits, presented at PEPM 2023.
-
What I learned formalizing category theory in Agda,
Topos Institute Colloquium, Sept. 23, 2022.
The video of that talk is available on YouTube.
-
Deriving on Steroids -- for proof assistants at
Dagstuhl meeting 18341 on Formalization of Mathematics in Type Theory.
Aug. 20th, 2018.
- Joint Lab meeting: From structured theories to efficient code
in 6 easy steps, March 9, 2012;
slides (pdf) available, but
they are hard to understand without the commentary -- ask me, I love this
give this talk!
- Joint PLMMS/Calculemus invited talk: Mechanized Mathematics
given July 8th in Paris, France. The
slides are inspired by the
Takahashi method
and only tell part of the story.
- 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).
Preprints and Technical Reports
- J. Carette, C. Heunen, R. Kaarsgaard, A. Sabry
With a Few Square Roots, Quantum Computing is as easy as Π. Under submission.
- G.M. Smith, J. Carette
Building Test Cases for Video Game-Focused Computational Models of Emotion,
submitted to a workshop, 2023.
- J. Carette, C. Heunen, R. Kaarsgaard, A. Sabry
The Quantum Effect: A Recipe for QuantumPi, Feb 2023 version (on arXiv). Under submission.
- G.M. Smith, J. Carette
Start your EMgine -- A Methodology for Choosing Emotion Theories for Computational Models of Emotion, submitted to a journal. 2023.
- J Carette, G Ortiz, A Sabry
Retrodictive Quantum Execution.
Available on arXiv.
There is also a github repository with all the code. May 2022.
- S. Smith, J. Carette,
Long-term Productivity Based on Science, not Preference, 2021. Available on arXiv.
- W.S. Smith, J. Carette, P. Michalski, A. Dong, O. Owojiye,
Methodology for assessing the state of the practice for domain X, 2021. Available on arXiv.
- J. Carette, R. O'Connor, Y. Sharoda
Building on the Diamonds between Theories: Theory Presentation Combinators, Oct. 2020 version.
(Nov. 2019 version available as an arxiv preprint),
Submitted. Completely rewritten version of CICM 2012 paper.
- J Carette, A Sabry
Optics and Type Equivalences
some preliminary thoughts on the relations between Optics and Type Equivalences.
Needs a rewrite, but interested people might still enjoy it in its current state.
- Noel Brett, Jacques Carette, Gabriel Dalimonte, Adele Olejarz, Geneva Smith and Sasha Soraine
Discussing The Effects of Visual Scaling on Games,
submitted to a conference.
- J. Carette, S. Soraine
Understanding the Player-Game Relationship through Challenges and Cognitive & Motor Abilities.
preprint version of a rejected paper. Will get re-submitted.
- S Smith, Y Sun, J Carette
Statistical software for psychology: Comparing development practices between CRAN and other communities,
(arxiv preprint, 2018)
- WS Smith, A Lazzarato, J Carette
State of the Practice for GIS Software,
(arXiv preprint, 2018).
- B. Yorgey, J. Carette, S. Weirich
Labelled structures and combinatorial species
- R.P. James, Z. Sparks, J. Carette and A. Sabry,
Fractional Types.
2013 preprint. Warning: the results are correct, but not nearly
as useful as hoped for...
- J. Carette, James H. Davenport
The Power of Vocabulary: The Case of Cyclotomic Polynomials (arXiv:1002.0012).
- 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
- J Carette, D Aspinall, C Lange, P Sojka, W Windsteiger,
Intellingent Computer Mathematics 2013
LNAI 7961, Proceedings of CICM 2013.
- J Jeuring, J Campbell, J Carette, G Dos Reis, P Sojka, M Wenzel, V Sorge
Intellingent Computer Mathematics 2012
LNAI 7362, Proceedings of CICM 2012.
- Carette, J.; Dixon, L.; Sacerdoti Coen, C.; Watt, S. (Eds.)
Intelligent Computer Mathematics 2009, LNAI 5625, Proceedings of CICM 2009
- J. Carette, W.M. Farmer (Eds.) ENTCS Volume 151, Number 1, March 2006 (special issue on Calculemus 2005).
- J. Carette, M. Wenzel, F. Wiedijk (Eds.),
special issue of Journal of Automated Reasoning on PLMMS 2007 and 2008)
Theses
Home