Sökning: onr:"swepub:oai:DiVA.org:ltu-73010" >
Introducing Certifi...
-
Lindgren, PerLuleå tekniska universitet,Datavetenskap
(författare)
Introducing Certified Compilation in Education by a Functional Language Approach
- Artikel/kapitelEngelska2019
Förlag, utgivningsår, omfång ...
-
Open Publishing Association,2019
-
printrdacarrier
Nummerbeteckningar
-
LIBRIS-ID:oai:DiVA.org:ltu-73010
-
https://urn.kb.se/resolve?urn=urn:nbn:se:ltu:diva-73010URI
-
https://doi.org/10.4204/EPTCS.295.5DOI
Kompletterande språkuppgifter
-
Språk:engelska
-
Sammanfattning på:engelska
Ingår i deldatabas
Klassifikation
-
Ämneskategori:ref swepub-contenttype
-
Ämneskategori:kon swepub-publicationtype
Anmärkningar
-
Classes on compiler technology are commonly found in Computer Science curricula, covering aspects of parsing, semantic analysis, intermediate transformations and target code generation. This paper reports on introducing certified compilation techniques through a functional language approach in an introductory course on Compiler Construction. Targeting students with little or no experience in formal methods, the proof process is highly automated using the Why3 framework. Underlying logic, semantic modelling and proofs are introduced along with exercises and assignments leading up to a formally verified compiler for a simplistic imperative language.This paper covers the motivation, course design, tool selection, and teaching methods, together with evaluations and suggested improvements from the perspectives of both students and teachers.
Ämnesord och genrebeteckningar
Biuppslag (personer, institutioner, konferenser, titlar ...)
-
Lindner, MarcusLuleå tekniska universitet,Datavetenskap(Swepub:ltu)maalin
(författare)
-
Fitinghoff, NilsLuleå tekniska universitet,Datavetenskap(Swepub:ltu)nilfit-3
(författare)
-
Luleå tekniska universitetDatavetenskap
(creator_code:org_t)
Sammanhörande titlar
-
Ingår i:Proceedings Seventh International Workshop on Trends in Functional Programming in Education: Open Publishing Association, s. 65-78
Internetlänk