| 2008 | Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL. | Amine Chaieb |
| 2008 | Case Studies in Model Manipulation for Scientific Computing. | Jacques Carette, W. Spencer Smith, John McCutchan, Christopher Kumar Anand, Alexandre Korobkine |
| 2008 | High-Level Theories. | Jacques Carette, William M. Farmer |
| 2008 | Automating Signature Evolution in Logical Theories. | Alan Bundy |
| 2008 | Digital Mathematics Libraries: The Good, the Bad, the Ugly. | Thierry Bouche |
| 2008 | Logic-Free Reasoning in Isabelle/Isar. | Stefan Berghofer, Makarius Wenzel |
| 2008 | Validated Evaluation of Special Mathematical Functions. | Franky Backeljauw, Stefan Becuwe, Annie A. M. Cuyt |
| 2008 | A Tactic Language for Hiproofs. | David Aspinall, Ewen Denney, Christoph Lth |
| 2008 | MetiTarski: An Automatic Prover for the Elementary Functions. | Behzad Akbarpour, Lawrence C. Paulson |
| 2008 | Applying Link Grammar Formalism in the Development of English-Indonesian Machine Translation System. | Teguh Bharata Adji, Baharum Baharudin, Norshuhani Zamin |
| 2006 | Hierarchical Representations with Signatures for Large Expression Management. | Wenqin Zhou, Jacques Carette, David J. Jeffrey, Michael B. Monagan |
| 2006 | Finding Relations Among Linear Constraints. | Jun Yan, Jian Zhang, Zhongxing Xu |
| 2006 | Quantifier Elimination for Quartics. | Lu Yang, Bican Xia |
| 2006 | Implicitization of Rational Curves. | Yongli Sun, Jianping Yu |
| 2006 | On the Mixed Cayley-Sylvester Resultant Matrix. | Weikun Sun, Hongbo Li |
| 2006 | A Full System of Invariants for Third-Order Linear Partial Differential Operators. | Ekaterina Shemyakova |
| 2006 | Constraints for Continuous Reachability in the Verification of Hybrid Systems. | Stefan Ratschan, Zhikun She |
| 2006 | Enhanced Theorem Reuse by Partial Theory Inclusions. | Immanuel Normann |
| 2006 | Labeled @-Calculus: Formalism for Time-Concerned Human Factors. | Tetsuya Mizutani, Shigeru Igarashi, Yasuwo Ikeda, Masayuki Shio |
| 2006 | The Confluence Problem for Flat TRSs. | Ichiro Mitsuhashi, Michio Oyamaguchi, Florent Jacquemard |
| 2006 | A New Definition for Passivity and Its Relation to Coherence. | Moritz Minzlaff, Jacques Calmet |
| 2006 | Semantic Guidance for Saturation Provers. | William McCune |
| 2006 | Using Hajs' Construction to Generate Hard Graph 3-Colorability Instances. | Sheng Liu, Jian Zhang |
| 2006 | An Algorithm for Computing the Complete Root Classification of a Parametric Polynomial. | Songxin Liang, David J. Jeffrey |
| 2006 | Some Properties of Triangular Sets and Improvement Upon Algorithm CharSer. | Yong-Bin Li |