Back to Search Start Over

Scallina: Translating Verified Programs from Coq to Scala

Authors :
Dani Mezher
Youssef El Bakouny
Source :
Programming Languages and Systems ISBN: 9783030027674, APLAS
Publication Year :
2018
Publisher :
Springer International Publishing, 2018.

Abstract

This paper presents the Scallina prototype: a new tool which allows the translation of verified Coq programs to Scala. A typical workflow features a user implementing a functional program in Gallina, the core language of Coq, proving this program’s correctness with regards to its specification and making use of Scallina to synthesize readable Scala components.

Subjects

Subjects :
Functional programming
Correctness
Scala
Programming language
Computer science
06 humanities and the arts
02 engineering and technology
0603 philosophy, ethics and religion
computer.software_genre
Formal methods
Workflow
020204 information systems
060302 philosophy
0202 electrical engineering, electronic engineering, information engineering
Compiler
Software_PROGRAMMINGLANGUAGES
computer
Core language
computer.programming_language

Details

ISBN :
978-3-030-02767-4
ISBNs :
9783030027674
Database :
OpenAIRE
Journal :
Programming Languages and Systems ISBN: 9783030027674, APLAS
Accession number :
edsair.doi...........3b9c6b320543e35f0ac5ee81d50bc842
Full Text :
https://doi.org/10.1007/978-3-030-02768-1_7
Full Text Access
View/download PDF

Tools

Authors Abstract Subjects Details