| |
|
|
| |
| | Jacques Carette is an associate professor of computer science and software engineering in the Department of Computing and Software at McMaster University, in Hamilton, Canada.¿He received his BMath from the University of Waterloo, MS from the Université de Montréal, and PhD (in pure mathematics) from the Université de Paris-Sud.¿Before joining academia, he worked for Maplesoft Inc. for 11 years, with roles ranging from math developer to product development director. His current research is centered on mechanized mathematics, joining computer algebra and theorem-proving facilities into a single system.¿He has emphasized the use of techniques from modern programming languages as well as meta-programming in his efforts to build a next-generation system. He also enjoys applying these techniques to the certified software area, and to improving software engineering strategies for game design. |
| |
| |
|
Date Reviewed |
|
| |
1 - 10 of 26
reviews
|
|
|
 |
|
|
|
|
A predicate transformer semantics for effects (functional pearl)
Swierstra W., Baanen T. Proceedings of the ACM on Programming Languages 3(ICFP): 1-26, 2019. Type: Article
Proving properties of imperative programs with side effects is quite arduous. Purely functional code, on the other hand, has a relatively pleasant equational theory that enables reasonable proofs. Is it possible to use modern machinery...
|
Jan 20 2021 |
|
|
|
|
|
|
Modular product programs
Eilers M., Müller P., Hitz S. ACM Transactions on Programming Languages and Systems 42(1): 1-37, 2019. Type: Article
Some properties of programs are not about a single run of the program; instead, they relate multiple runs. For example, a program is deterministic if, given the same input, two runs will always produce the same answer. Many other prope...
|
Jan 14 2020 |
|
|
|
|
|
|
 Computational mathematics with SageMath
Zimmermann P., Casamayou A., Cohen N., Connan G., Dumont T., Fousse L., Maltey F., Meulien M., Mezzarobba M., Pernet C., Thiry N., Bray E., Cremona J., Forets M., Ghitza A., Thomas H., SIAM-Society for Industrial and Applied Mathematics, Philadelphia, PA, 2018. 464 pp. Type: Book (978-1-611975-45-1)
SageMath is by now a well-established system for computational mathematics. It is used by many researchers, as well as increasingly in classrooms. While there is a wealth of material online to learn it, including many published papers,...
|
Sep 23 2019 |
|
|
|
|
|
|
Hammer for Coq: automation for dependent type theory
Czajka Ł., Kaliszyk C. Journal of Automated Reasoning 61(1-4): 423-453, 2018. Type: Article
Interactive theorem proving is today seeing an explosion of use similar to what computer algebra systems (CASs) saw in the late 1980s. But there is another aspect to mathematics that CASs do not do: reasoning and proofs....
|
Jan 3 2019 |
|
|
|
|
|
|
Conditioning in probabilistic programming
Olmedo F., Gretz F., Jansen N., Kaminski B., Katoen J., Mciver A. ACM Transactions on Programming Languages and Systems 40(1): 1-50, 2018. Type: Article
Machine learning, possibly contrary to popular belief, is not just about endless variations of neural networks. There is also a thriving subculture of probabilistic programming based on Bayesian principles. A large advantage of the lat...
|
Jun 13 2018 |
|
|
|
|
|
|
Bit-precise procedure-modular termination analysis
Chen H., David C., Kroening D., Schrammel P., Wachter B. ACM Transactions on Programming Languages and Systems 40(1): 1-38, 2018. Type: Article
That software is pervasive in our lives is now a platitude. That much of this software is flawed has also reached the collective consciousness. A lot of code, much to the chagrin of most researchers in programming languages, is still w...
|
Apr 27 2018 |
|
|
|
|
|
|
A semantic framework for proof evidence
Chihani Z., Miller D., Renaud F. Journal of Automated Reasoning 59(3): 287-330, 2017. Type: Article
The use of theorem provers as fundamental aids in computer science and software engineering is slowly expanding their reach. The multitude of tools and methods does have a downside: lack of interoperability. It would be nice if, for ex...
|
Feb 6 2018 |
|
|
|
|
|
|
Markov chains and Markov decision processes in Isabelle/HOL
Hölzl J. Journal of Automated Reasoning 59(3): 345-387, 2017. Type: Article
The intermingling of rather different domains can, at times, produce rather interesting results. Here the author explores the intersection of probability theory (in the guise of Markov chains and Markov decision processes) and formal p...
|
Jan 11 2018 |
|
|
|
|
|
|
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
Aransay J., Divasón J. Formal Aspects of Computing 28(6): 1005-1026, 2016. Type: Article
Formalization is rapidly evolving from being highly desirable but thought too difficult to be realistic, to being quite feasible and well on its way to being expected. The raw technology of theorem provers certainly is ready. What is s...
|
Mar 9 2017 |
|
|
|
|
|
|
Verified functional programming in Agda
Stump A., Association for Computing Machinery and Morgan & Claypool, New York, NY, 2016. 284 pp. Type: Book (978-1-970001-24-2)
Verification used to be a daunting task, to be performed only in extreme circumstances, at great cost. Our knowledge of how to perform verification, at least for certain kinds of code, has progressed so much that there are now textbook...
|
Oct 28 2016 |
|
|
|
|
|
| |
|
|
| |
|
|
