TPHOLs 2004 |
|
| Time | Event |
|---|---|
| 9:00-10:00 | Registration |
| 10:00-11:00 | Session 1 Invited Talk,
Ken McMillan Applications of Craig Interpolation to Model Checking |
| 11-11:30 | Break |
| 11:30-12:30 | Session 2 Hardware Verification |
| 11:30-12:00 | Behzad Akbarpour and Sofiene Tahar Error Analysis of Digital Filters using Theorem Proving |
| 12:00-12:30 | Michael Jones, Aaron Benson, and Dan Delorey Proving Compatibility using Refinement |
| 12:30-14:30 | Lunch |
| 14:30-16:00 | Session 3 Proof Technology |
| 14:30-15:00 | Olivier Boite Proof Reuse with Extended Inductive Types |
| 15:00-15:30 | Einar Broch Johnsen and Christoph Lueth Theorem Reuse by Proof Term Transformation |
| 15:30-16:00 | Lee Pike, Jeffrey Maddalon, Paul Miner, and Alfons Geser Abstractions for Fault-Tolerant Distributed System Verification |
| 16:00-16:30 | Break |
| 16:30-17:00 | Session 4 Poster Talks |
| 17:00-18:00 | Poster Presentation |
| Time | Event |
|---|---|
| 9:00-10:00 | Session 5
Invited Talk, Thomas Hales Formalizing the Proof of the Kepler Conjecture |
| 10-10:30 | Break |
| 10:30-12:00 | Session 6 Mathematics Verification |
| 10:30-11:00 | Luis Cruz-Filipe and Freek Wiedijk Hierarchical Reflection |
| 11:00-11:30 | Ruben Gamboa and John Cowles A Mechanical Proof of the Cook-Levin Theorem |
| 11:30-12:00 | Stefan Richter Formalizing Integration Theory, with an Application to Probabilistic Algorithms |
| 12:00-14:30 | Lunch |
| 14:30-16:00 | Session 7 Program Logics |
| 14:30-15:00 | David Aspinall, Lennart Beringer, Martin Hofmann,
Hans-Wolfgang Loidl, and Alberto Momigliano A Program Logic for Resource Verification |
| 15:00-15:30 | Nadeem Abdul Hamid and Zhong Shao Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code |
| 15:30-16:00 | John Longley and Randy Pollack Reasoning About CBV Functional Programs in Isabelle/HOL |
| 16:00-16:30 | Break |
| 16:30-17:00 | Session 8 Poster Talks |
| 17:00-18:00 | Poster Presentation |
| Time | Event |
|---|---|
| 9:00-10:00 | Session 9 Logical Frameworks |
| 9:00-9:30 | Penny Anderson and Frank Pfenning Verifying Uniqueness in a Logical Framework |
| 9:30-10:00 | Jason Hickey and Aleksey Nogin Extensible Hierarchical Tactic Construction in a Logical Framework |
| 10:00-10:30 | Break |
| 10:30-12:00 | Session 10 Program Logics |
| 10:30-11:00 | Martin Wildmoser and Tobias Nipkow Certifying machine code safety: shallow versus deep embedding |
| 11:00-11:30 | Hanbing Liu and J Moore Java Program Verification via a JVM Deep Embedding in ACL2 |
| 11:30-12:00 | Zuo Tian-Jun, Han Jun-Gang, and Chen Ping Formalizing Java Dynamic Loading in HOL |
| 12:00-18:00 | Excursion to Snowbird |
| Evening | Banquet at Riverhorse |
| Time | Event |
|---|---|
| 9:00-10:00 | Session 11
Invited Talk, Al Davis Correct Embedded Computing Futures |
| 10:00-10:30 | Break |
| 10:30-12:00 | Session 12 Proof Automation |
| 10:30-11:00 | Lucas Dixon and Jacques Fleuriot Higher Order Rippling in IsaPlanner |
| 11:00-11:30 | Julien Narboux A Decision Procedure for Geometry in Coq |
| 11:30-12:00 | Ting Zhang, Henny B. Sipma, and Zohar Manna Term Algebras with Length Function and Bounded Quantifier Alternation |
| 12:00-14:30 | Lunch |
| 14:30-15:30 | Session 13 |
| 14:30-15:00 | Jean-Francois Monin Proof Pearl: From concrete to functional unparsing |
| 15:00-15:30 | Michael Norrish Recursive function definition for types with binders |
| 15:30-16:00 | Break |
| 16:00-17:00 | Business Meeting |
| End of Conference |
|
|
TPHOLs / tphols2004@cs.utah.edu |
|