Publication
Scaling Language Features for Program Verification
Publications associées (134)
Trust as a Programming Primitive
Programming has changed; programming languages have not.Modern software embraced reusable software components, i.e., public libraries, and runs in the cloud, on machines that co-locate applications from various origins.This new programming paradigm leads t ...
EPFL2021Representing Monads with Capabilities
Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Jonathan Immanuel Brachthäuser
Programming with monads can be advantageous even in imperative languages with builtin support for side effects. However, in these languages composing monadic programs is different from composing side effecting imperative programs. This does not need to be ...
2021Formal Verification of Rust with Stainless
Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of ...
2021Stoic: Towards Disciplined Capabilities
Martin Odersky, Nada Amin, Fengyun Liu, Sandro Stucki, Paolo Giosuè Giarrusso
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 ...
2020Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages
Software engineering practices have been steadily moving towards higher-level programming languages and away from lower-level ones. High-level languages tend to greatly improve safety, productivity, and code maintainability because they handle various impl ...
EPFL2020Finally, a Polymorphic Linear Algebra Language
Amir Shaikhha, Lionel Emile Vincent Parreaux
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 ...
2019Refutation-based synthesis in SMT
Viktor Kuncak, Andrew Joseph Reynolds
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided ...
SPRINGER2019A Programming Model and Foundation for Lineage-Based Distributed Computation
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, or middleware, upon which to build data-centric distribute ...
Cambridge University Press2018