Publications related to Generalized algebraic data type

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Dotty Phantom Types

Martin Odersky, Nicolas Alexander Stucki

Phantom types are a well-known type-level, design pattern which is commonly used to express constraints encoded in types. We observe that in modern, multi-paradigm programming languages, these encodings are too restrictive or do not provide the guarantees ...

2017

Adaptive WENO methods based on radial basis functions reconstruction

Jan Sickmann Hesthaven, Caterina Bigoni

We explore the use of radial basis functions (RBF) in the weighted essentially non-oscillatory (WENO) reconstruction process used to solve hyperbolic conservation laws, resulting in a numerical method of arbitrarily high order to solve problems with discon ...

Springer Verlag2017

Data Reconciliation for Reaction Systems Using Extents and Shape Constraints

Dominique Bonvin, Julien Léo Billeter, Sriniketh Srinivasan

Concentrations measured during the course of reactions are typically corrupted by random noise. Data reconciliation techniques improve the accuracy of measurements by using redundancies in the material and energy balances expressed as relationships between ...

Elsevier2017

A Generic Algorithm for Checking Exhaustivity of Pattern Matching

Fengyun Liu

Algebraic data types and pattern matching are key features of functional programming languages. Exhaustivity checking of pattern matching is a safety belt that defends against unmatched exceptions at runtime and boosts type safety. However, the presence of ...

Assoc Computing Machinery2016

Automating Verification of Functional Programs with Quantified Invariants

Viktor Kuncak, Nicolas Charles Yves Voirol

We present the foundations of a verifier for higher-order functional programs with generics and recursive algebraic data types. Our ver- ifier supports finding sound proofs and counterexamples even in the presence of certain quantified invariants and recur ...

2016

Verifying Resource Bounds of Programs with Lazy Evaluation and 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 eval- uation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. ...

2016

A TASTY Alternative

Martin Odersky, Eugene Burmako, Dmytro Petrashko

This document proposes a new serialization format for typed syntax trees of Scala programs. It aims to be ● compact: All numbers and references are length encoded, trees are inlined by default but may be shared. ● lazy: Trees can be explored from the top, ...

2016

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

Generalized algebraic data type

Graph Chatbot

Chat with Graph Search

Dotty Phantom Types

Adaptive WENO methods based on radial basis functions reconstruction

Data Reconciliation for Reaction Systems Using Extents and Shape Constraints

A Generic Algorithm for Checking Exhaustivity of Pattern Matching

A generic algorithm for checking exhaustivity of pattern matching

Automating Verification of Functional Programs with Quantified Invariants

Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization

A TASTY Alternative

SMT-Based Checking of Predicate-Qualified Types for Scala

Dependent Object Types

Automating Verification of Functional Programs with Quantified Invariants

Adaptive WENO methods based on radial basis functions reconstruction

A Generic Algorithm for Checking Exhaustivity of Pattern Matching

Dependent Object Types

Dotty Phantom Types

A generic algorithm for checking exhaustivity of pattern matching

SMT-Based Checking of Predicate-Qualified Types for Scala

Data Reconciliation for Reaction Systems Using Extents and Shape Constraints

A TASTY Alternative

Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization