Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

You searched for id:"oai:infoscience.epfl.ch:268824". One record found.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters


EPFL

1. Voirol, Nicolas Charles Yves. Verified Functional Programming.

Degree: 2019, EPFL

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solvers to automate the verification process and to provide us with useful counterexamples when considered properties are invalid. We then enable verification in the presence of high-level Scala language features by encoding them into the dependently-typed language. We introduce an SMT-backed counterexample finding procedure which can also prove that no counterexample exists. The procedure incrementally unfolds function calls and applications in order to progressively explore the space of counterexamples. We present increasingly expressive fragments of our dependently-typed language and establish soundness and completeness properties of the procedure for each fragment. We then describe an extension which introduces support for quantifier reasoning. We discuss syntactic and semantic conditions under which the extended procedure can produce valid counterexamples in the presence of universal quantification. We present a bidirectional type checking algorithm for our dependent type system. The algorithm relies on our counterexample finding procedure to discharge verification conditions which enables predictable and effective type checking. The type system features a unified treatment of both recursive and corecursive definitions, and further admits mutual recursion between type and function definitions. We establish normalization through a sized types approach. We define a logical relation which associates a set of reducible values to each type, and then show soundness of verification by proving that evaluation of a type checked expression terminates with a reducible value. We further discuss a set of transformations which encode high-level Scala constructs into our dependently-typed language. These transformations allow our verification system to support object-oriented features such as traits and classes with multiple inheritance, as well as abstract and concrete methods with overriding. We further present a measure inference transformation which enables automated termination checking in our system. In addition to encoding language features, we discuss how Scala can be augmented with natural specification constructs and annotations that empower verification. Finally, we describe the system implementation and discuss certain practical considerations. We show that the resulting system is effective by evaluating it on a set of benchmarks and case studies comprising over 15K lines of Scala code. These benchmarks showcase both the breadth and flexibility of the system.

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Voirol, N. C. Y. (2019). Verified Functional Programming. (Thesis). EPFL. Retrieved from http://infoscience.epfl.ch/record/268824/files/EPFL_TH9479.pdf ; http://infoscience.epfl.ch/record/268824

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16th Edition):

Voirol, Nicolas Charles Yves. “Verified Functional Programming.” 2019. Thesis, EPFL. Accessed October 19, 2019. http://infoscience.epfl.ch/record/268824/files/EPFL_TH9479.pdf ; http://infoscience.epfl.ch/record/268824.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7th Edition):

Voirol, Nicolas Charles Yves. “Verified Functional Programming.” 2019. Web. 19 Oct 2019.

Vancouver:

Voirol NCY. Verified Functional Programming. [Internet] [Thesis]. EPFL; 2019. [cited 2019 Oct 19]. Available from: http://infoscience.epfl.ch/record/268824/files/EPFL_TH9479.pdf ; http://infoscience.epfl.ch/record/268824.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Voirol NCY. Verified Functional Programming. [Thesis]. EPFL; 2019. Available from: http://infoscience.epfl.ch/record/268824/files/EPFL_TH9479.pdf ; http://infoscience.epfl.ch/record/268824

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

.