Campus Event Calendar
Event Entry
New for: D1, D2, D3, D4, D5
What and Who
Proof Assistant and Formalization of "Types and Programming Languages" with Isabelle HOL
Michaël Noël Divo
International Max Planck Research School for Computer Science - IMPRS
IMPRS Research Seminar
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 4 January 2016
12:05
30 Minutes
E1 4
024
Saarbrücken
Abstract
Having only a nice paper proof is not enough anymore today to convince
reviewers. Thus the need of formal proofs grows up and the best way to
obtain such a valid proof is using a Proof Assistant.
As a contribution to such Proof Assistants, I'll present the still
unformalized parts of the book: "Types and Programming Languages", that I
intend to formalize. A big effort awaits me, but this will grant other
users access to a collection of nice results related to Program Analysis
and a lot of other fields.
Finally, my goal is also to make you aware of possibilities given by Proof
Assistants, future researchs' topics in this domain and the benefit implied
by progress in this field.
reviewers. Thus the need of formal proofs grows up and the best way to
obtain such a valid proof is using a Proof Assistant.
As a contribution to such Proof Assistants, I'll present the still
unformalized parts of the book: "Types and Programming Languages", that I
intend to formalize. A big effort awaits me, but this will grant other
users access to a collection of nice results related to Program Analysis
and a lot of other fields.
Finally, my goal is also to make you aware of possibilities given by Proof
Assistants, future researchs' topics in this domain and the benefit implied
by progress in this field.
Contact
Andrea Ruffing
--email hidden
passcode not visible
logged in users only
Andrea Ruffing, 01/04/2016 10:21 -- Created document.