ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 12:00 - 12:30 at SUN II - Program Analysis and Automated Verification Chair(s): Stephanie Balzer

We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolution is recast in terms of coinductive uniform proofs; its constructive content is exposed via soundness relative to an intuitionistic first-order logic with recursion controlled by the later modality; and soundness of both proof systems is proven relative to novel coalgebraic interpretation of complete Herbrand models.

Thu 11 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:30: Program Analysis and Automated VerificationESOP at SUN II
Chair(s): Stephanie BalzerCarnegie Mellon University
10:30 - 11:00
Talk
ESOP
Link to publication
11:00 - 11:30
Talk
ESOP
Matthieu Journault, Antoine MinéUPMC, France, Abdelraouf OuadjaoutSorbonne Université
Link to publication
11:30 - 12:00
Talk
ESOP
Carsten FuhsBirkbeck, University of London, Cynthia KopRadboud University Nijmegen
Link to publication
12:00 - 12:30
Talk
ESOP
Henning BasoldCNRS & ENS Lyon, Ekaterina KomendantskayaHeriot-Watt University, UK, Yue LiHeriot-Watt University, UK
Link to publication