| |
|
|
| |
| | 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 70
reviews
|
|
|
 |
|
|
|
|
Photoplethysmogram-based cognitive load assessment using multi-feature fusion model
Zhang X., Lyu Y., Qu T., Qiu P., Luo X., Zhang J., Fan S., Shi Y. ACM Transactions on Applied Perception 16(4): 1-17, 2019. Type: Article
Physiological measures of cognitive load have become more accessible with advancements in neuro-imaging devices and wearable technology, and provide quantifiable data that previous measurement tools (for example, surveys) could not. As...
|
Oct 8 2021 |
|
|
|
|
|
|
Quantum relational Hoare logic
Unruh D. Proceedings of the ACM on Programming Languages 3(POPL): 1-31, 2019. Type: Article
All programs need to be verified--even post-quantum cryptography software. To prove properties of such protocols requires proofs that involve not only quantum programming, but also pairs of programs, an encryptor and an attack...
|
Jan 22 2021 |
|
|
|
|
|
|
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 |
|
|
|
|
|
|
 Bayesian synthesis of probabilistic programs for automatic data modeling
Saad F., Cusumano-Towner M., Schaechtle U., Rinard M., Mansinghka V. Proceedings of the ACM on Programming Languages 3(POPL): 1-32, 2019. Type: Article
Somewhat overshadowed by neural networks (NN) is another thread in machine learning: the Bayesian-based approach. Less data hungry, it also has the promise of being closer to explainable artificial intelligence (XAI), although it hasn&...
|
Jun 3 2020 |
|
|
|
|
|
|
Metamorphic testing: a review of challenges and opportunities
Chen T., Kuo F., Liu H., Poon P., Towey D., Tse T., Zhou Z. ACM Computing Surveys 51(1): 1-27, 2018. Type: Article
Testing software remains a complex business, so finding different means for doing so is important. Metamorphic testing belongs in one’s toolkit, along with unit tests and property-based testing. Thus, overviews are particular...
|
Jun 2 2020 |
|
|
|
|
|
|
Smart assisted living: toward an open smart-home infrastructure
Chen F., García-Betances R., Chen L., Cabrera-Umpiérrez M., Nugent C., Springer International Publishing, New York, NY, 2019. 342 pp. Type: Book (978-3-030255-89-3)
With an aging population and an ever-growing connection of smart devices, there hasn’t been a more appropriate time for this type of book. Ubiquitous computing has revolutionized the way that health can be managed. Equipping ...
|
Feb 5 2020 |
|
|
|
|
|
|
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 |
|
|
|
|
|
|
Knowledge management in theory and practice (3rd ed.)
Dalkir K., The MIT Press, Cambridge, MA, 2017. 552 pp. Type: Book (978-0-262036-87-0)
When building software, whether we realize it or not, we embed various kinds of knowledge into it. Software engineers doing requirements gathering and domain analysis have realized this, as have programming language researchers when th...
|
Jan 18 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 |
|
|
|
|
|
| |
|
|
| |
|
|
