[Club2] IJCAR & FLoC dry runs, updated updated schedule

[Jasmin Christian Blanchette]

Dear yokefellows,

Tobias found another flaw in my dry run schedule: I scheduled a talk on a holiday (June 3). So here's the updated updated schedule, with (I hope) no talks on holidays:


IJCAR 2010
Monotonicity Inference for Higher-Order Logic
(joint work with Alex)
http://www4.in.tum.de/~blanchet/ijcar2010-mono.pdf
Tue. June 8, 2010 at 14:00 in Turing (00.11.055)

Formulas are often monotonic in the sense that if the formula is satisfiable for given domains of discourse, it is also satisfiable for all larger domains. Monotonicity is undecidable in general, but we devised two calculi that infer it in many cases for higher-order logic. The stronger calculus has been implemented in Isabelle’s model finder Nitpick, where it is used to prune the search space, leading to dramatic speed improvements for formulas involving many atomic types.


TAP 2010
Relational Analysis of (Co)inductive Predicates, (Co)inductive Datatypes, and (Co)recursive Functions
http://www4.in.tum.de/~blanchet/tap2010-relational.pdf
Tue. June 15, 2010 at 14:00 in Turing (00.11.055)

This paper presents techniques for applying a finite relational model finder to logical specifications that involve (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. In contrast to previous work, which focused on algebraic datatypes and restricted occurrences of unbounded quantifiers in formulas, we can handle arbitrary formulas by means of a three-valued Kleene logic. The techniques form the basis of the counterexample generator Nitpick for Isabelle/HOL. As a case study, we consider a coalgebraic lazy list type.


The TAP talk has significant overlap with today's ITP talk, so you might want to skip it (but it would be nice to have one or two volunteers nonetheless).

Thanks for today's feedback, and hope to see you there!

Jasmin