BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Structural Resolution meets Curry-Howard - Ekateri
na Komendantskaya (Dundee)
DTSTART:20151106T130000Z
DTEND:20151106T140000Z
UID:TALK1877AT
URL:/talk/index/1877
DESCRIPTION:Mathematical induction is pervasive in programming
and program\nverification. It arises in data defi
nitions (e.g.\, it describes some\nalgebraic data
structures)\, it underlies program semantics (e.g.
\, it\nexplains how to reason about finite iterati
on and recursion)\, and it\ngets used in proofs (e
.g.\, it supports lemmas about data structures use
d\nin inductive proofs). Coinduction\, too\, is im
portant in programming and\nprogram verification.
It arises in infinite data definitions (e.g.\,\nla
zily defined infinite streams)\, semantics (e.g.\,
of concurrency)\, and\nproofs (e.g.\, of observat
ional equivalence of potentially infinite\nprocess
es). It is thus desirable to have good support for
both induction\nand coinduction in systems for re
asoning about programs.\n\n\nThe first implementat
ions of coinduction were pioneered in Calculus of\
nCoinductive Constructions (CIC) in the 90s\, wher
e the duality of\ninductive and coinductive method
s was achieved by distinguishing\ninductive from c
oinductive types\, recursive functions consuming i
nputs\nof inductive types from corecursive functio
ns producing outputs of\ncoinductive types\, and i
nductive proof methods from coinductive proof\nmet
hods.\n\n\n\nRecently\, the rapid development of a
utomated theorem proving (ATP) has opened the way
to introducing induction and coinduction to ATP. S
ome coinductive methods of ITP can be easily trans
lated to ATPs. For example\, definitions of (induc
tive and) coinductive types in ITP translate natur
ally into fixed-point definitions in ATP. However\
, some coinductive methods in ITP are much trickie
r to adapt to ATP: e.g.\, the theory of universal
productivity of corecursive functions or coinduct
ive proof principles.\n\nStructural resolution is
a newly introduced proof method for Horn Clause lo
gic that can replace the classical SLD-resolution\
, and promises to deliver a ``missing link” theor
y that merges automation of ATP and constructive c
oinductive methods of ITP. In this talk I will gi
ve Type-theoretic semantics to Structural resoluti
on\, and will show how it gives rise to automated
version of coinductive proofs known in CIC. \n\
nJoint work with John Power\, Patricia Johann\, Pe
ng Fu.
LOCATION:CS 217
CONTACT:Neel Krishnaswami
END:VEVENT
END:VCALENDAR