<span itemscope itemtype="http://schema.org/InformAction"><span style="display:none" itemprop="about" itemscope itemtype="http://schema.org/Person"><meta itemprop="description" content="Einladung von piller@in.tum.de"/></span><span itemprop="object" itemscope itemtype="http://schema.org/Event"><div style=""><table cellspacing="0" cellpadding="8" border="0" summary="" style="width:100%;font-family:Arial,Sans-serif;border:1px Solid #ccc;border-width:1px 2px 2px 1px;background-color:#fff;"><tr><td><meta itemprop="eventStatus" content="http://schema.org/EventScheduled"/><h4 style="padding:6px 0;margin:0 0 4px 0;font-family:Arial,Sans-serif;font-size:13px;line-height:1.4;border:1px Solid #fff;background:#fff;color:#090;font-weight:normal"><strong>Sie wurden zum folgenden Termin eingeladen.</strong></h4><div style="padding:2px"><span itemprop="publisher" itemscope itemtype="http://schema.org/Organization"><meta itemprop="name" content="Google Calendar"/></span><meta itemprop="eventId/googleCalendar" content="0e0mph6ikqdqchkf8unggjdh6d"/><h3 style="padding:0 0 6px 0;margin:0;font-family:Arial,Sans-serif;font-size:16px;font-weight:bold;color:#222"><span itemprop="name">Generalizing Isabelle's Lifting Package</span></h3><table style="display:inline-table" cellpadding="0" cellspacing="0" border="0" summary="Termindetails"><tr><td style="padding:0 1em 10px 0;font-family:Arial,Sans-serif;font-size:13px;color:#888;white-space:nowrap;width:90px" valign="top"><div><i style="font-style:normal">Wann</i></div></td><td style="padding-bottom:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222" valign="top"><div style="text-indent:-1px"><time itemprop="startDate" datetime="20220518T120000Z"></time><time itemprop="endDate" datetime="20220518T123000Z"></time>Mi 18. Mai 2022 14:00 – 14:30 <span style="color:#888">Mitteleuropäische Zeit - Berlin</span></div></td></tr><tr><td style="padding:0 1em 10px 0;font-family:Arial,Sans-serif;font-size:13px;color:#888;white-space:nowrap;width:90px" valign="top"><div><i style="font-style:normal">Wo</i></div></td><td style="padding-bottom:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222" valign="top"><div style="text-indent:-1px"><span itemprop="location" itemscope itemtype="http://schema.org/Place"><span itemprop="name" class="notranslate">http://tinyurl.com/ls21coffee</span><span dir="ltr"> (<a href="https://www.google.com/url?q=http%3A%2F%2Ftinyurl.com%2Fls21coffee&sa=D&ust=1652692453614000&usg=AOvVaw0CNl6CB-UjYwxsv99hueXC" style="color:#20c;white-space:nowrap" target="_blank" itemprop="map">Karte</a>)</span></span></div></td></tr><tr><td style="padding:0 1em 10px 0;font-family:Arial,Sans-serif;font-size:13px;color:#888;white-space:nowrap;width:90px" valign="top"><div><i style="font-style:normal">Kalender</i></div></td><td style="padding-bottom:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222" valign="top"><div style="text-indent:-1px">club2@in.tum.de</div></td></tr><tr><td style="padding:0 1em 10px 0;font-family:Arial,Sans-serif;font-size:13px;color:#888;white-space:nowrap;width:90px" valign="top"><div><i style="font-style:normal">Wer</i></div></td><td style="padding-bottom:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222" valign="top"><table cellspacing="0" cellpadding="0"><tr><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222;width:10px"><div style="text-indent:-1px"><span style="font-family:Courier New,monospace">•</span></div></td><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222"><div style="text-indent:-1px"><div><div style="margin:0 0 0.3em 0"><span class="notranslate">piller@in.tum.de</span><span style="font-size:11px;color:#888">- Veranstalter</span></div></div></div></td></tr><tr><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222;width:10px"><div style="text-indent:-1px"><span style="font-family:Courier New,monospace">•</span></div></td><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222"><div style="text-indent:-1px"><div><div style="margin:0 0 0.3em 0"><span itemprop="attendee" itemscope itemtype="http://schema.org/Person"><span itemprop="name" class="notranslate">j.gottfriedsen@tum.de</span><meta itemprop="email" content="j.gottfriedsen@tum.de"/></span></div></div></div></td></tr><tr><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222;width:10px"><div style="text-indent:-1px"><span style="font-family:Courier New,monospace">•</span></div></td><td style="padding-right:10px;font-family:Arial,Sans-serif;font-size:13px;color:#222"><div style="text-indent:-1px"><div><div style="margin:0 0 0.3em 0"><span itemprop="attendee" itemscope itemtype="http://schema.org/Person"><span itemprop="name" class="notranslate">club2@in.tum.de</span><meta itemprop="email" content="club2@in.tum.de"/></span></div></div></div></td></tr></table></td></tr></table><div style="float:right;font-weight:bold;font-size:13px"> <a href="https://calendar.google.com/calendar/event?action=VIEW&eid=MGUwbXBoNmlrcWRxY2hrZjh1bmdnamRoNmQgY2x1YjJAaW4udHVtLmRl&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTU1MmYyNmQwNDJhMDg2ZGU3MGRhNDJlMTZhZjNlNmNmNDZkYjk0Yjg&ctz=Europe%2FBerlin&hl=de&es=0" style="color:#20c;white-space:nowrap" itemprop="url">Mehr Details »</a><br></div><div style="padding-bottom:15px;font-family:Arial,Sans-serif;font-size:13px;color:#222;white-space:pre-wrap!important;white-space:-moz-pre-wrap!important;white-space:-pre-wrap!important;white-space:-o-pre-wrap!important;white-space:pre;word-wrap:break-word"><span>Speaker: Juli Gottfriedsen<br>Type: Guided Research Presentation<br>Abstract:<br>The transfer and lifting packages of Isabelle/HOL<br>allow users to automatically translate statements and definitions between different types.<br>However, the latter is tailored to work with the static type system of Isabelle/Pure<br>and expects its transfer relations to be right-total and right-unique.<br>As such, it cannot be used to lift terms in a soft type systems,<br>as recently explored in Isabelle/Set.<br>We present a generalization of the lifting package that<br>relaxes the conditions put on its transfer relations and,<br>in particular, allows users to lift terms between soft types.<br>We verified the theoretic foundations of our approach in Isabelle/HOL<br>and propose a generalized lifting algorithm.</span><meta itemprop="description" content="Speaker: Juli Gottfriedsen
Type: Guided Research Presentation
Abstract:
The transfer and lifting packages of Isabelle/HOL
allow users to automatically translate statements and definitions between different types.
However, the latter is tailored to work with the static type system of Isabelle/Pure
and expects its transfer relations to be right-total and right-unique.
As such, it cannot be used to lift terms in a soft type systems,
as recently explored in Isabelle/Set.
We present a generalization of the lifting package that
relaxes the conditions put on its transfer relations and,
in particular, allows users to lift terms between soft types.
We verified the theoretic foundations of our approach in Isabelle/HOL
and propose a generalized lifting algorithm."/></div></div><p style="color:#222;font-size:13px;margin:0"><span style="color:#888">Teilnehmen (club2@in.tum.de)? </span><wbr><strong><span itemprop="potentialaction" itemscope itemtype="http://schema.org/RsvpAction"><meta itemprop="attendance" content="http://schema.org/RsvpAttendance/Yes"/><span itemprop="handler" itemscope itemtype="http://schema.org/HttpActionHandler"><link itemprop="method" href="http://schema.org/HttpRequestMethod/GET"/><a href="https://calendar.google.com/calendar/event?action=RESPOND&eid=MGUwbXBoNmlrcWRxY2hrZjh1bmdnamRoNmQgY2x1YjJAaW4udHVtLmRl&rst=1&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTU1MmYyNmQwNDJhMDg2ZGU3MGRhNDJlMTZhZjNlNmNmNDZkYjk0Yjg&ctz=Europe%2FBerlin&hl=de&es=0" style="color:#20c;white-space:nowrap" itemprop="url">Ja</a></span></span><span style="margin:0 0.4em;font-weight:normal"> - </span><span itemprop="potentialaction" itemscope itemtype="http://schema.org/RsvpAction"><meta itemprop="attendance" content="http://schema.org/RsvpAttendance/Maybe"/><span itemprop="handler" itemscope itemtype="http://schema.org/HttpActionHandler"><link itemprop="method" href="http://schema.org/HttpRequestMethod/GET"/><a href="https://calendar.google.com/calendar/event?action=RESPOND&eid=MGUwbXBoNmlrcWRxY2hrZjh1bmdnamRoNmQgY2x1YjJAaW4udHVtLmRl&rst=3&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTU1MmYyNmQwNDJhMDg2ZGU3MGRhNDJlMTZhZjNlNmNmNDZkYjk0Yjg&ctz=Europe%2FBerlin&hl=de&es=0" style="color:#20c;white-space:nowrap" itemprop="url">Vielleicht</a></span></span><span style="margin:0 0.4em;font-weight:normal"> - </span><span itemprop="potentialaction" itemscope itemtype="http://schema.org/RsvpAction"><meta itemprop="attendance" content="http://schema.org/RsvpAttendance/No"/><span itemprop="handler" itemscope itemtype="http://schema.org/HttpActionHandler"><link itemprop="method" href="http://schema.org/HttpRequestMethod/GET"/><a href="https://calendar.google.com/calendar/event?action=RESPOND&eid=MGUwbXBoNmlrcWRxY2hrZjh1bmdnamRoNmQgY2x1YjJAaW4udHVtLmRl&rst=2&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTU1MmYyNmQwNDJhMDg2ZGU3MGRhNDJlMTZhZjNlNmNmNDZkYjk0Yjg&ctz=Europe%2FBerlin&hl=de&es=0" style="color:#20c;white-space:nowrap" itemprop="url">Nein</a></span></span></strong> <wbr><a href="https://calendar.google.com/calendar/event?action=VIEW&eid=MGUwbXBoNmlrcWRxY2hrZjh1bmdnamRoNmQgY2x1YjJAaW4udHVtLmRl&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTU1MmYyNmQwNDJhMDg2ZGU3MGRhNDJlMTZhZjNlNmNmNDZkYjk0Yjg&ctz=Europe%2FBerlin&hl=de&es=0" style="color:#20c;white-space:nowrap" itemprop="url">Weitere Optionen »</a></p></td></tr><tr><td style="background-color:#f6f6f6;color:#888;border-top:1px Solid #ccc;font-family:Arial,Sans-serif;font-size:11px"><p>Einladung von <a href="https://calendar.google.com/calendar/" target="_blank" style="">Google Kalender</a></p><p>Sie erhalten diese E-Mail unter club2@in.tum.de, da Sie ein Gast bei diesem Termin sind.</p><p>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.</p><p>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. <a href="https://support.google.com/calendar/answer/37135#forwarding">Weitere Informationen</a>.</p></td></tr></table></div></span></span>