Publications associées à Pure type system

Formal Foundations of Capture Tracking

Type systems are a device for verifying properties of programs without running them. Many programming languages used in the industry have always had a type system, while others were initially created without a type system and later adopted one, when the ad ...

EPFL2024

Degrees of Separation: A Flexible Type System for Safe Concurrency

Martin Odersky, Yichen Xu, Aleksander Slawomir Boruch-Gruszecki

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

2024

Capturing Types

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Ondrej Lhoták

Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC

Assoc Computing Machinery2023

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy

Lionel Emile Vincent Parreaux

MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bi ...

2020

Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages

Lionel Emile Vincent Parreaux

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

EPFL2020

Modelling of the tensile behavior of SH-UHPFRC at low and high stress levels, under very low loading rates

Emmanuel Denarié, Mohamed Abdul Hafiz

The tensile behavior under low loading rates governs to a large extend the mechanical response of Strain Hardening Ultra High Performance Fiber Reinforced Concretes (SH-UHPFRC) at early age and long term, in applications of rehabilitation. A viscoelastic-v ...

2020

Influence of low curing temperatures on the tensile response of low clinker Strain Hardening UHPFRC under full restraint

Emmanuel Denarié, Mohamed Abdul Hafiz

The tensile response of strain hardening UHPFRC under full restraint, subjected to curing temperatures of 20 °C, 10 °C, 5 °C, was investigated for two types of mixes with silica fume; Mix I with pure type I cement and Mix II with 50% replacement of cement ...

Pergamon-Elsevier Science Ltd2020

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

Monotonicity Types for Distributed Dataflow

Heather Christine Klug

The Lasp programming language provides combinator functions such as Union and Intersection for combining set CRDTs. When designing a CRDT combinator, care must be taken to ensure that the combinator is monotone separately in each of its arguments, so that ...

2017

Monotonicity Types

Heather Christine Klug

In the face of the increasing trend in application development to interact with more and more remote services, and cognizant of the fact that issues arising from data consistency and task coordination are core challenges in distributed programming, the sys ...

2017