Publications associées à Lambda cube

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning

Yichen Xu, Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies ...

Assoc Computing Machinery2022

On the probability distribution of the local times of diagonally operator-self-similar Gaussian fields with stationary increments

Thomas Mountford, Kamran Kalbasi

In this paper, we study the local times of vector-valued Gaussian fields that are 'diagonally operator-selfsimilar' and whose increments are stationary. Denoting the local time of such a Gaussian field around the spatial origin and over the temporal unit h ...

INT STATISTICAL INST2020

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

Implementing Higher-Kinded Types in Dotty

Martin Odersky, Guillaume André Fradji Martres, Dmytro Petrashko

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

Chiral charge erasure via thermal fluctuations of magnetic helicity

Eray Sabancilar

We consider a relativistic plasma of fermions coupled to an Abelian gauge field and carrying a chiral charge asymmetry, which might arise in the early Universe through baryogenesis. It is known that on large length scales, lambda greater than or similar to ...

Iop Publishing Ltd2016

Complete Completion using Types and Weights

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes ...

ACM2013

Decision Procedures for Algebraic Data Types with Abstractions

Viktor Kuncak, Philippe Paul Henri Suter, Mirco Dotta

We describe a family of decision procedures that extend the decision procedure for quantifier-free constraints on recursive algebraic data types (term algebras) to support recursive abstraction functions. Our abstraction functions are catamorphisms (term a ...

2010

Programming language abstractions for mobile code

Stéphane Micheloud

Scala is a general-purpose programming language developed at EPFL. It combines the most important concepts found in object-oriented and functional languages. Scala is a statically typed language; in particular it features an advanced type system and suppor ...

EPFL2009

Full Functional Verification of Linked Data Structures

Viktor Kuncak

We present the first verification of full functional correctness for a range of linked data structure implementations, including mutable lists, trees, graphs, and hash tables. Specifically, we present the use of the Jahob verification system to verify form ...

2008

Inversion de Fourier ponctuelle

Emanuel Enrico Seifert

Let f be an integrable function on RN, a a point in RN and B a complex number. If the mean value of f on the sphere of centre a and radius r tends to B when r tends to 0, we show that the Fourier integral at a of f is summable to B in Cesàro means of order ...

EPFL2007