University of Birmingham > Talks@bham > Theoretical computer science seminar > Structural Resolution meets Curry-Howard

## Structural Resolution meets Curry-HowardAdd to your list(s) Download to your calendar using vCal - Ekaterina Komendantskaya (Dundee)
- Friday 06 November 2015, 13:00-14:00
- CS 217.
If you have a question about this talk, please contact Neel Krishnaswami. Mathematical induction is pervasive in programming and program verification. It arises in data definitions (e.g., it describes some algebraic data structures), it underlies program semantics (e.g., it explains how to reason about finite iteration and recursion), and it gets used in proofs (e.g., it supports lemmas about data structures used in inductive proofs). Coinduction, too, is important in programming and program verification. It arises in infinite data definitions (e.g., lazily defined infinite streams), semantics (e.g., of concurrency), and proofs (e.g., of observational equivalence of potentially infinite processes). It is thus desirable to have good support for both induction and coinduction in systems for reasoning about programs. The first implementations of coinduction were pioneered in Calculus of Coinductive Constructions (CIC) in the 90s, where the duality of inductive and coinductive methods was achieved by distinguishing inductive from coinductive types, recursive functions consuming inputs of inductive types from corecursive functions producing outputs of coinductive types, and inductive proof methods from coinductive proof methods. Recently, the rapid development of automated theorem proving (ATP) has opened the way to introducing induction and coinduction to ATP . Some coinductive methods of ITP can be easily translated to ATPs. For example, definitions of (inductive and) coinductive types in ITP translate naturally into fixed-point definitions in ATP . However, some coinductive methods in ITP are much trickier to adapt to ATP : e.g., the theory of universal productivity of corecursive functions or coinductive proof principles. Structural resolution is a newly introduced proof method for Horn Clause logic that can replace the classical SLD -resolution, and promises to deliver a ``missing link” theory that merges automation of ATP and constructive coinductive methods of ITP . In this talk I will give Type-theoretic semantics to Structural resolution, and will show how it gives rise to automated version of coinductive proofs known in CIC . Joint work with John Power, Patricia Johann, Peng Fu. This talk is part of the Theoretical computer science seminar series. ## This talk is included in these lists:- CS 217
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Theoretical computer science seminar
Note that ex-directory lists are not shown. |
## Other listsMolecular and Medical Physics Seminar Series Analysis seminar Particle Physics Seminars## Other talksThe highwater algebra The imprint of their explosions: Using supernova remnants to understand stellar death Discrete models of cellular mechanics |