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 solve ...
Many different data analytics tasks boil down to linear algebra primitives. In practice, for each different type of workload, data scientists use a particular specialised library. In this paper, we present Pilatus, a polymorphic iterative linear algebra la ...
Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...
The insertion of an InGaN underlayer (UL) is known to strongly improve the performance of InGaN/GaN quantum well (QW) based blue light emitting diodes (LEDs). However, the actual physical mechanism responsible for it is still unclear. We thus conduct a sys ...
As of today, programming has never been so accessible. Yet, it remains a challenge for end-users: students, non-technical employees, experts in their domains outside of computer science, and so on. With its forecast potential for solving problems by only o ...
The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate on which to build data-centric distributed systems. A key id ...
Statically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages ...
Software development has taken a fundamental turn. Software today has gone from simple, closed programs running on a single machine, to massively open programs, patching together user experiences byway of responses received via hundreds of network requests ...