Publication

Accelerating Interpolants

Publications associées (32)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Formal foundations for GADTs in Scala

GADTs are a very useful language feature that allow encoding some invariants in types. GADT reasoning is currently implemented in Scala and Dotty, but it’s plagued with soundness issues. To get a better understanding of GADTs in Scala, we explore how they ...

2020

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

Higher-Order Subtyping with Type Intervals

Sandro Stucki

Modern, statically typed programming languages provide various abstraction facilities at both the term- and type-level. Common abstraction mechanisms for types include parametric polymorphism -- a hallmark of functional languages -- and subtyping -- which ...

EPFL2017

, ,

dotty is a new, experimental Scala compiler based on DOT, the calculus of Dependent Object Types. Higher-kinded types are a natural extension of first-order lambda calculus, and have been a core construct of Haskell and Scala. As long as such types are jus ...

ACM2016

SMT-Based Checking of Predicate-Qualified Types for Scala

Viktor Kuncak, Georg Stefan Schmid

We present qualified types for Scala, a form of refinement types adapted to the Scala language. Qualified types allow users to refine base types and classes using predicate expressions. We implemented a type checker for qualified types that is embedded in ...

Assoc Computing Machinery2016

Decrypting Local Type Inference

Hubert Plociniczak

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

EPFL2016

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. In particular, objects can contain type members, which can be selected as ...

EPFL2016

Verification of Component-based Systems via Predicate Abstraction and Simultaneous Set Reduction

Simon Bliudze, Qiang Wang

This paper presents a novel safety property verification approach for component-based systems modelled in BIP (Behaviour, Interaction and Priority), encompassing multiparty synchronisation with data transfer and priority. Our contributions consist of: (1 ...

Springer2015

Language Support for Distributed Functional Programming

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

EPFL2015

Functional programming (FP) is regularly touted as the way forward for bringing parallel, concurrent, and distributed programming to the mainstream. The popularity of the rationale behind this viewpoint (immutable data transformed by function application) ...

2014