Publications related to Generalized algebraic data type

Automated Formal Verification of Software Network Functions

Formally verifying the correctness of software is necessary to merit the trust people put in software systems. Currently, formal verification requires human effort to prove that a piece of code matches its specification and code changes to improve verifiab ...

EPFL2024

Privacy-Preserving Machine Learning on Graphs

Sina Sajadmanesh

Graph Neural Networks (GNNs) have emerged as a powerful tool for learning on graphs, demonstrating exceptional performance in various domains. However, as GNNs become increasingly popular, new challenges arise. One of the most pressing is the need to ensur ...

EPFL2023

CellCharter reveals spatial cell niches associated with tissue remodeling and cell plasticity

Daniele Tavernari, Albert Santamaria Martinez, Giovanni Ciriello

Tissues are organized in cellular niches, the composition and interactions of which can be investigated using spatial omics technologies. However, systematic analyses of tissue composition are challenged by the scale and diversity of the data. Here we pres ...

Nature Portfolio2023

Preprocessing Antarctic Weather Station (AWS) data in python

Michael Lehning, Franziska Gerber

There are many sources providing atmospheric weather station data for the Antarctic continent. However, variable naming, timestamps and data types are highly variable between the different sources. The published python code intends to make processing of di ...

Zenodo2022

Virtual ADTs for Portable Metaprogramming

Martin Odersky, Nicolas Alexander Stucki

Scala 3 provides a metaprogramming interface that represents the abstract syntax tree definitions using algebraic data types. To allow the compiler to freely evolve without breaking the metaprogramming interface, we present virtual algebraic data types (or ...

ASSOC COMPUTING MACHINERY2021

Synthesis of Flexible Accelerators for Early Adoption of Ring-LWE Post-quantum Cryptography

Francesco Regazzoni, Subhadeep Banik, Hamid Nejatollahi

The advent of the quantum computer makes current public-key infrastructure insecure. Cryptography community is addressing this problem by designing, efficiently implementing, and evaluating novel public-key algorithms capable of withstanding quantum comput ...

ASSOC COMPUTING MACHINERY2020

Multi-omics reveals abundant mitochondrial genomic and circadian expression variation in the Drosophila Genetic Reference Panel

Maria Litovchenko

Modern biology rapidly generates a wealth of data,which can only be analysed computationally.Despite the variety of available data types,most of them aim to provide an answer to one question: how does genotypic diversity translates into phenotypes? This qu ...

EPFL2020

Contact networks across ages: computational analysis of epidemiological dynamics

Gianrocco Lazzari

For decades mathematical modeling in epidemiology has helped understanding the dynamics of infectious diseases, as well as describe possible intervention scenarios to prevent and control them. However, such models were relying on several assumptions, such ...

EPFL2020

Towards Improved GADT Reasoning in Scala

Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki, Paolo Giosuè Giarrusso

Generalized algebraic data types (GADT) have been notoriously difficult to implement correctly in Scala. Both major Scala compilers, Scalac and Dotty, are currently known to have type soundness holes related to them. In particular, covariant GADTs have exp ...

ASSOC COMPUTING MACHINERY2019

Refutation-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 ...

SPRINGER2019

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

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 ...

EPFL2019

Composite Data Types in Dynamic Dataflow Languages as Copyless Memory Sharing Mechanism

Marco Mattavelli, Endri Bezati, Aurélien François Gilbert Bloch

This paper presents new optimization approaches aiming at reducing the impact of memory accesses on the performance of dataflow programs. The approach is based on introducing a high level management of composite data types in dynamic dataflow programming l ...

2019

Verified Functional Programming

Nicolas Charles Yves Voirol

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 ...

EPFL2019

Truly abstract interfaces for algebraic data types: the extractor typing problem

Martin Odersky, Nicolas Alexander Stucki, Paolo Giosuè Giarrusso

Pattern matching enables inspecting algebraic data types, but typically prevents hiding the implementation of the matched algebraic data type. In Scala, instead, extractors also allow pattern matching on non-algebraic data types and invoking methods on the ...

2018

On subadditivity of Kodaira dimension in positive characteristic over a general type base

Zsolt Patakfalvi

We show that for a surjective, separable morphism f of smooth projective varieties over a field of positive characteristic such that f(*) OX congruent to O-Y subadditivity of Kodaira dimension holds, provided the base is of general type and the Hasse-Witt ...

2018

Network utility maximization for delay-sensitive applications in unknown communication settings

Stefano D'Aronco

In the last decades the Internet traffic has greatly evolved. The advent of new Internet services and applications has, in fact, led to a significant growth of the amount of data transmitted, as well as to a transformation of the data type. As a matter of ...

EPFL2018

Algorithmic Resource Verification

Ravichandhran Kandhadai Madhavan

Static estimation of resource utilisation of programs is a challenging and important problem with numerous applications. In this thesis, I present new algorithms that enable users to specify and verify their desired bounds on resource usage of functional p ...

EPFL2017

An Update on Deductive Synthesis and Repair in the Leon Tool

Viktor Kuncak, Emmanouil Koukoutos, Etienne Kneuss

We report our progress in scaling deductive synthesis and repair of recursive functional Scala programs in the Leon tool. We describe new techniques, including a more precise mechanism for encoding the space of meaningful candidate programs. Our techniques ...

2017

Contract-Based Resource Verification for Higher-Order Functions with Memoization

Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. a ...

Assoc Computing Machinery2017

SmarPer: Context-Aware and Automatic Runtime-Permissions for Mobile Devices

Jean-Pierre Hubaux, Kévin Clément Huguenin, Italo Ivan Dacosta Petrocelli, Joana Catarina Soares Machado, Mohammad Emtiyaz Khan, Katarzyna Lucja Olejnik

Permission systems are the main defense that mobile platforms, such as Android and iOS, offer to users to protect their private data from prying apps. However, due to the tension between usability and control, such systems have several limitations that oft ...

IEEE2017