Scala has been developed as a language that deeply integrates with the Java ecosystem. It offers seamless interoperability with existing Java libraries. Since the Scala compiler targets Java bytecode, Scala programs have access to high-performance runtimes ...
Capabilities are widely used in the design of software systems to ensure security. A system of capabilities can become a mess in the presence of objects and functions: objects may leak capabilities and functions may capture capabilities. They make reasonin ...
Several useful variance-reduced stochastic gradient algorithms, such as SVRG, SAGA, Finito, and SAG, have been proposed to minimize empirical risks with linear convergence properties to the exact minimizer. The existing convergence results assume uniform d ...
The inception of object-oriented programming introduces a category of bugs related to object construction: initialization errors. Every newly created object goes through several initialization states: starting from a state where all fields are uninitialize ...
Inlining is used in many different ways in programming languages: some languages use it as a compiler-directive solely for optimization, some use it as a metaprogramming feature, and others lay their design in-between. This paper presents inlining through ...
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 ...
