onr:"swepub:oai:DiVA.org:ltu-73010"
Search: onr:"swepub:oai:DiVA.org:ltu-73010" > Introducing Certifi...
- 1 of 1
- Previous record
- Next record
- To hitlist
- Lindgren, PerLuleå tekniska universitet,Datavetenskap (author)
Introducing Certified Compilation in Education by a Functional Language Approach
- Article/chapterEnglish2019
Publisher, publication year, extent ...
- Open Publishing Association,2019
- printrdacarrier
Numbers
- 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
Supplementary language notes
- Language:English
- Summary in:English
Part of subdatabase
- SwePubSwePub
Classification
Notes
- 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.
Subject headings and genre
- TEKNIK OCH TEKNOLOGIER Elektroteknik och elektronik Inbäddad systemteknik hsv//swe
- ENGINEERING AND TECHNOLOGY Electrical Engineering, Electronic Engineering, Information Engineering Embedded Systems hsv//eng
- Dependable Communication and Computation Systems
- Kommunikations- och beräkningssystem
Added entries (persons, corporate bodies, meetings, titles ...)
- Lindner, MarcusLuleå tekniska universitet,Datavetenskap(Swepub:ltu)maalin (author)
- Fitinghoff, NilsLuleå tekniska universitet,Datavetenskap(Swepub:ltu)nilfit-3 (author)
- Luleå tekniska universitetDatavetenskap (creator_code:org_t)
Related titles
- In:Proceedings Seventh International Workshop on Trends in Functional Programming in Education: Open Publishing Association, s. 65-78
Internet link
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Lindgren, Per
- Lindner, Marcus
- Fitinghoff, Nils
- About the subject
-
- ENGINEERING AND TECHNOLOGY
- ENGINEERING AND ...
- and Electrical Engin ...
- and Embedded Systems
- Articles in the publication
- Proceedings Seve ...
- By the university
- Luleå University of Technology
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
