Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

New for: D1, D2, D3, D4, D5
<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Proof Assistant and Formalization of "Types and Programming Languages" with Isabelle HOL
Speaker:Michaël Noël Divo
coming from:International Max Planck Research School for Computer Science - IMPRS
Speakers Bio:
Event Type:IMPRS Research Seminar
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Language:English
Date, Time and Location
Date:Monday, 4 January 2016
Time:12:05
Duration:30 Minutes
Location:Saarbrücken
Building:E1 4
Room:024
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.
Contact
Name(s):Andrea Ruffing
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
Created by:Andrea Ruffing/MPI-INF, 01/04/2016 10:18 AMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Andrea Ruffing, 01/04/2016 10:21 AM -- Created document.