UNIF 2009
August 2, 2009. Montreal, Canada

UNIF Workshop Schedule

Invited Talk
09:00 - 10:00 Catherine Meadows:
A Cryptographer's Garden of Equational Theories: Interesting Unification Problems from Cryptography
Regular papers UNIF/ADDCT
10:30 - 11:00 UNIF: Michael Franssen:
Implementing Rigid E-Unification
11:00 - 11:30 UNIF: Sunil Kothari, James Caldwell:
A Machine Checked Model of MGU Axioms: Applications of Finite Maps and Functional Induction
11:30 - 12:00 UNIF: Temur Kutsia, Mircea Marin:
Order-Sorted Unification with Regular Expression Sorts
12:00 - 12:30 ADDCT: Sergey Babenyshev, Vladimir Rybakov, Renate A. Schmidt, Dmitry Tishkovsky:
A Tableau Method for Checking Rule Admissibility in S4
Work in progress/Presentation only papers (ADDCT)
14:00 - 14:30 ADDCT: Grant Olney Passmore, Leonardo de Moura:
Universality of Polynomial Positivity and a Variant of Hilbert's 17th Problem
14:30 - 14:55 ADDCT: Renate A. Schmidt:
The Ackermann Approach for Modal Logic, Correspondence Theory and Second-Order Reduction
14:55 - 15:20 ADDCT: Lan Zhang, Ullrich Hustadt, Clare Dixon:
CTL-RP: A Computational Tree Logic Resolution Prover
Work in progress/Presentation only papers (UNIF)
16:00-16:25 UNIF: Pascal Fontaine:
Combinations of theories for decidable fragments of first-order logic
16:25-16:50 UNIF: Franz Baader and Barbara Morawska:
Unification in the Description Logic EL
16:50-17:15 UNIF: Enrica Nicolini, Christophe Ringeissen and Michael Rusinowitch:
Decision Procedures for Data Structures Combined with Shared Fragments of Arithmetic
17:15-17:40 UNIF: Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran and Michael Rusinowitch:
Cap Unification: Application to Protocol Security modulo Homomorphic Encryption
17:45 - 18:00 UNIF Business meeting