[Club2] Einladung: Towards Automated Proofs in Higher-Order Concurrent Separ... - Mi 22. Jun. 2022 14:00 - 14:25 (MESZ) (club2 at in.tum.de)

[piller at in.tum.de]

Sie wurden zum folgenden Termin eingeladen.

Titel: Towards Automated Proofs in Higher-Order Concurrent Separation Logic
Speaker: Florian Sextl
Abstract: The Iris framework implemented in Coq allows defining  
higher-order concurrent program logics based on separation logic. This work  
investigates how well that framework can be ported to Isabelle/HOL and  
whether the proof automation for such a port can be as efficient as or  
better than in Coq. To this end, a partial port of Iris has been developed  
that contains all necessary facilities to work with selectedreal-world  
examples. In this process, we analyzed how Coq features used by Iris can be  
translated to Isabelle and found that the whole framework can in general be  
recreated there, although with certain caveats. A full port is necessarily  
more verbose with regard to composable proofs and requires either an  
axiomatic extension to HOL or an mapping from syntax to semantics outside  
of the logic depending on how the Iris logicis embedded. In another step,  
we developed specialized proof automation methods for our Iris port and  
compared them with existing Coq machinery for the same purpose. To this  
end, we developed translation techniques for common mechanization patterns  
from Coq to Isabelle. We conclude that at least in the context of the Iris  
logic neither Isabelle nor Coq provide significantly stronger proof  
automation compared to the othersystem.
Wann: Mi 22. Jun. 2022 14:00 – 14:25 Mitteleuropäische Zeit - Berlin
Wo: Seminarraum 00.09.038
Kalender: club2 at in.tum.de
Wer
     * piller at in.tum.de- Veranstalter
     * club2 at in.tum.de
     * brandtf at in.tum.de
     * liedtke at ma.tum.de
     * mitja.krebs at tum.de
     * r.dardjonova at gmail.com
     * madlener at in.tum.de
     * sextl at in.tum.de
     * rimpapa at in.tum.de

Termininformationen:  
https://calendar.google.com/calendar/event?action=VIEW&eid=N2h2Ym81ZHQ4ZmIycDJmN3E1b3RqZDdjYTIgY2x1YjJAaW4udHVtLmRl&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTM1OTE3ODgxNWNkZWQ2M2JiNmMwNmY3ZTdiMTg5YjkxNGI1ZDdkNWU&ctz=Europe%2FBerlin&hl=de&es=0

Einladung von Google Kalender: https://calendar.google.com/calendar/

Sie erhalten diese E-Mail unter club2 at in.tum.de, da Sie ein Gast bei diesem  
Termin sind.

Lehnen Sie diesen Termin ab, um keine weiteren Informationen zu diesem  
Termin zu erhalten. Sie können auch unter  
https://calendar.google.com/calendar/ ein Google-Konto erstellen und Ihre  
Benachrichtigungseinstellungen für Ihren gesamten Kalender steuern.

Wenn Sie diese Einladung weiterleiten, kann jeder Empfänger eine Antwort an  
den Organisator senden und zur Gästeliste hinzugefügt werden. Außerdem  
könnte er weitere Nutzer einladen und Ihre Antwort ändern. Weitere  
Informationen: https://support.google.com/calendar/answer/37135#forwarding
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20220620/41df63ab/attachment-0001.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 3655 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20220620/41df63ab/attachment-0001.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 3719 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20220620/41df63ab/attachment-0001.bin>