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

- Drasil, a framework
for
*generating all the things* - Hakaru (and its documentation), a probabilistic programming language.
- Experiments (in Agda and Haskell) in reversible programming. Includes code for "computing with semirings and ..." paper.
- HOL Light QE, adding Quote and Eval to HOL Light.
- GenCheck, a generalized QuickCheck-like package that allows you to vary the sampling strategy, from enumerative to probabilistic (and many others) without having to rewrite your tests.
- And the thoroughly obsolete pa_monad

- Theories and Data-Structures wherein we attempt to show that some mathematical theories and some (functional) data-structures are inextricably linked.

- The Agda standard library
- I am even sort-of the maintainer of 'the' category theory library for Agda.

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

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

*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)

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

Home