Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
projects [2016/11/15 17:02] vkuncak |
projects [2017/04/11 11:43] vkuncak |
||
|---|---|---|---|
| Line 13: | Line 13: | ||
| Below we list several projects reflecting the current interests of our research group. All projects can be adapted to fit the scope of a semester project (bachelor & master) or master's project. | Below we list several projects reflecting the current interests of our research group. All projects can be adapted to fit the scope of a semester project (bachelor & master) or master's project. | ||
| - | Many of these project are based on the [[http://lara.epfl.ch/w/leon|Leon system]] for synthesis and verification. We suggest that you get the basic idea of Leon in any case. Please note that we release software under open source licenses and we request our contributors to agree that EPFL LARA holds copyright of the code that you contribute. | + | Many of these project are based on the [[http://lara.epfl.ch/w/leon|Leon system]] for synthesis and verification. We suggest that you get the basic idea of Leon in any case. |
| - | If you have your own idea, feel free to check with us, but please note that we some times cannot accommodate your own project suggestions even if the student is brilliant and the project is excellent. Moreover, even if you select one of the projects listed below, we reserve the right to not offer you the project. By deciding to talk to us you agree that you will not require detailed justification on why we made our negative decision. | + | **Licence for code:** Please note that we release software under open source licenses and we request our contributors to agree that EPFL LARA holds copyright of the code that you contribute. |
| + | |||
| + | **Disclaimer:** If you have your own idea, feel free to check with us, but please note that we some times cannot accommodate your own project suggestions even if the student is brilliant and the project is excellent. Moreover, even if you select one of the projects listed below, we reserve the right to not offer you the project. By deciding to talk to us you agree that you will not require detailed justification on why we made our negative decision. | ||
| + | |||
| + | === WebAssembly Generation Library for Scala === | ||
| + | |||
| + | Write a library for generating WebAssembly code, to be used in Computer Language Processing course as well as for other projects in the community. This library might replace the Cafebabe library: https://github.com/psuter/cafebabe | ||
| === Robust Front End for Leon Compiled Using scala.js === | === Robust Front End for Leon Compiled Using scala.js === | ||
| The goal of this task is to design a reasonably fast front end for the subset of Scala that is relevant for Leon. The front-end should be able to process existing regression test suite for Leon, but will necessarily deviate from scalac or dotty on some examples. In particular, the type system can be simpler and implicit resolution can be more restrictive than in Scala. Optionally, the front end may support omitting type declarations even for certain function parameters, if these can be inferred given a whole program using type inference for parametric types with simple structural subtyping. | The goal of this task is to design a reasonably fast front end for the subset of Scala that is relevant for Leon. The front-end should be able to process existing regression test suite for Leon, but will necessarily deviate from scalac or dotty on some examples. In particular, the type system can be simpler and implicit resolution can be more restrictive than in Scala. Optionally, the front end may support omitting type declarations even for certain function parameters, if these can be inferred given a whole program using type inference for parametric types with simple structural subtyping. | ||
| + | |||
| + | === Verifying JavaScript === | ||
| + | |||
| + | Design a translation of a clean subset of JavaScript including higher-order functions and (mostly immutable) objects into Leon. Map numbers into Double (apply overflow checks as needed), and enable annotations or special function calls to describe types and contracts. | ||
| + | |||
| + | Note that `(f:TObj) => e` can be encoded as `TObj(x => e)`. | ||
| + | |||
| + | === AST-Based Version Control === | ||
| + | |||
| + | Develop a layer on top of git for managing revisions of Leon programs at the level of high-level syntax tree transformations, with conflict resolution doing semantic commutativity checks. | ||
| === Easily editable and exportable hand-writing presentation videos === | === Easily editable and exportable hand-writing presentation videos === | ||
| Line 56: | Line 72: | ||
| This project likely requires the previous project on parameterized-length bitvectors. | This project likely requires the previous project on parameterized-length bitvectors. | ||
| - | === Verify Electronic Contract Code === | + | === Verify Smart Contract Code === |
| Verify correctness of electronic contract code. See, for example: | Verify correctness of electronic contract code. See, for example: | ||
| Line 101: | Line 117: | ||
| A version of Scala combinator library interface built on top of this library is also of interest, see e.g. (https://github.com/scala/scala-parser-combinators ). | A version of Scala combinator library interface built on top of this library is also of interest, see e.g. (https://github.com/scala/scala-parser-combinators ). | ||
| - | === THERE IS MORE === | + | ===== Contact us ===== |
| - | If a project you would like to do is not listed, but you are a student with high grades of substantial experience and have other ideas or interests, let us talk and explore if we can find a project that will interest you. | + | If one of the projects lists sounds interesting and you believe you are a suitable candide, please do not hesitate to contact Viktor Kuncak, http://lara.epfl.ch/~kuncak via email to make an appointment. In your email, please include your CV, the list of your grades, and a description of projects that you did at EPFL or outside of EPFL. |
| - | + | ||
| - | ===== Contact us ===== | + | |
| - | If one of the projects lists sounds interesting, or if you have other interests that you would like to pursue, do not hesitate to contact Viktor Kuncak, http://lara.epfl.ch/~kuncak via email to make an appointment. In your email, please include your CV, the list of your grades, and a description of projects that you did at EPFL or outside of EPFL. | + | Feel free to also talk to the other members of LARA group about their ongoing work and projects, see http://lara.epfl.ch |
| - | Feel free to also talk to the other members of LARA group about their work and project suggestions: http://lara.epfl.ch | ||