| 2007 | Formal Device and Programming Model for a Serial Interface. | Eyad Alkassar, Mark A. Hillebrand, Steffen Knapp, Rostislav Rusev, Sergey Tverdyshev |
| 2007 | Improvements in Formula Generalization. | Markus Aderhold |
| 2006 | Formal Global Optimisation with Taylor Models. | Roland Zumkeller |
| 2006 | The MathServe System for Semantic Web Reasoning Services. | Jrgen Zimmer, Serge Autexier |
| 2006 | Canonical Gentzen-Type Calculi with (n, k)-ary Quantifiers. | Anna Zamansky, Arnon Avron |
| 2006 | On the Strength of Proof-Irrelevant Type Theories. | Benjamin Werner |
| 2006 | Consistency and Completeness of Rewriting in the Calculus of Constructions. | Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz |
| 2006 | A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. | Christian Urban, Stefan Berghofer |
| 2006 | FaCT++ Description Logic Reasoner: System Description. | Dmitry Tsarkov, Ian Horrocks |
| 2006 | On Keys and Functional Dependencies as First-Class Citizens in Description Logics. | David Toman, Grant E. Weddell |
| 2006 | Using the TPTP Language for Writing Derivations and Finite Interpretations. | Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Allen Van Gelder |
| 2006 | CASC-J3 - The 3rd IJCAR ATP System Competition. | Geoff Sutcliffe |
| 2006 | Automatic Construction and Verification of Isotopy Invariants. | Volker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton |
| 2006 | Interpolation in Local Theory Extensions. | Viorica Sofronie-Stokkermans |
| 2006 | A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). | Erik Reeber, Warren A. Hunt Jr. |
| 2006 | First-Order Logic with Dependent Types. | Florian Rabe |
| 2006 | Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach. | Brigitte Pientka |
| 2006 | Connection Tableaux with Lazy Paramodulation. | Andrey Paskevich |
| 2006 | Importing HOL into Isabelle/HOL. | Steven Obua, Sebastian Skalberg |
| 2006 | Geometric Resolution: A Proof Procedure Based on Finite Model Search. | Hans de Nivelle, Jia Meng |
| 2006 | Flyspeck I: Tame Graphs. | Tobias Nipkow, Gertrud Bauer, Paula Schultz |
| 2006 | Representing and Reasoning with Operational Semantics. | Dale Miller |
| 2006 | An Interpretation of Isabelle/HOL in HOL Light. | Sean McLaughlin |
| 2006 | Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. | Assia Mahboubi |
| 2006 | Stratified Context Unification Is NP-Complete. | Jordi Levy, Manfred Schmidt-Schau, Mateu Villaret |