[Club2] Einladung: Development of a Linter for Isabelle - Mi 29. Sep. 2021 14:30 - 15:00 (MESZ) (club2 at mailbroy.informatik.tu-muenchen.de)
piller at in.tum.de
piller at in.tum.de
Thu Sep 9 09:03:14 CEST 2021
Sie wurden zum folgenden Termin eingeladen.
Titel: Development of a Linter for Isabelle
Speaker: Yecine MegdicheType: Bachelor's Thesis PresentationAbstract: While
the interactive theorem prover Isabelle can assist with developingintricate
formalizations leveraging the power of interactive proofs, not all ofthem
have the same quality. Indeed, some proofs might require a
highermaintenance effort or be harder to read and understand. Some of the
patternscausing these unwieldy formalizations are identified through the
years by theIsabelle community. A prominent resource demonstrating these
patterns and howto avoid them is Gerwin Klein’s Style Guide for
Isabelle/HOL. However, as itstands, there is no existing tool to
automatically warn users of these pitfallsor suggest better alternatives.
We attempt to fill this gap in the Isabelle environmentby developing an
Isabelle linter. The linter offers basic configurability,
extensibility,Isabelle/jEdit integration, and a standalone command-line
tool. With the helpof the 20 implemented checks, it uncovered 252 problems
in Isabelle/HOL, 28.97% of which are of high severity, 58.35 % of medium
severity, and 14.68 % of lowseverity. Adding to that, 20 randomly selected
entries from the Archive ofFormal Proofs are analyzed, which produced 575
lints distributed as follows: 45.39% of high severity, 44.17 % of medium
severity, and 10.43 % of low severity.
Wann: Mi 29. Sep. 2021 14:30 – 15:00 Mitteleuropäische Zeit - Berlin
Wo: htto://tinyurl.com/ls21coffee
Kalender: club2 at mailbroy.informatik.tu-muenchen.de
Wer
* piller at in.tum.de- Veranstalter
* club2 at mailbroy.informatik.tu-muenchen.de
* yecine.megdiche at gmail.com
Termininformationen:
https://calendar.google.com/calendar/event?action=VIEW&eid=NGxmMzBvcjBycGVpNmthMW40MGV2M2Y1OGogY2x1YjJAbWFpbGJyb3kuaW5mb3JtYXRpay50dS1tdWVuY2hlbi5kZQ&tok=NTIjc2U2ZWJlM3RvZmY0Y2g1bm11bmlibTVtOThAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbTVjMDdiODc1YjdlZjVlZDAzZTM4NmE2ZjJlZjgyMDdhMWU4YjliNWY&ctz=Europe%2FBerlin&hl=de&es=0
Einladung von Google Kalender: https://calendar.google.com/calendar/
Sie erhalten diese E-Mail unter club2 at mailbroy.informatik.tu-muenchen.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/20210909/b560bd00/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/calendar
Size: 2952 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210909/b560bd00/attachment.ics>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: invite.ics
Type: application/ics
Size: 3008 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/club2/attachments/20210909/b560bd00/attachment.bin>
More information about the Club2
mailing list