English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Formalization of Types and Programming Languages in Isabelle/HOL

Divo, M. N. (2017). Formalization of Types and Programming Languages in Isabelle/HOL. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is

Basic

show hide
Genre: Thesis
Latex : Formalization of Types and Programming Languages in Isabelle/{HOL}

Files

show Files
hide Files
:
2017_Michael Divo_MSc thesis.pdf (Any fulltext), 692KB
 
File Permalink:
-
Name:
2017_Michael Divo_MSc thesis.pdf
Description:
-
OA-Status:
Visibility:
Restricted (Max Planck Institute for Informatics, MSIN; )
MIME-Type / Checksum:
application/pdf
Technical Metadata:
Copyright Date:
-
Copyright Info:
-
License:
-

Locators

show

Creators

show
hide
 Creators:
Divo, Michael Noel1, Author
Blanchette, Jasmin Christian2, Advisor           
Weidenbach, Christoph2, Referee           
Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: -
 Abstract: Modern programming languages offer a lot of guarantees (no or few memory leaks, safe parallel programming, ...). But are they really safe ? The only solution is to formalize them and to prove that the expected properties are fulfilled. That’s why it is relevant to prove essential and general facts about programming languages like those presented in Types and Programming Languages, a reference book on type systems, in Isabelle/HOL. Isabelle/HOL is a proof assistant, providing type checking and certifying the consistency of proofs. This environment allowed me to discover some imprecision and wrong parts.

Details

show
hide
Language(s): eng - English
 Dates: 2017-05-242017
 Publication Status: Issued
 Pages: 83 p.
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: DivoMaster2017
 Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show