LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision Both sides next revision
projects [2016/11/15 17:08]
vkuncak
projects [2016/11/21 16:02]
vkuncak
Line 26: Line 26:
  
 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 ===