Publications related to Simply typed lambda calculus

Formal Autograding in a Classroom (Experience Report)

Viktor Kuncak, Mario Bucev, Dragana Milovancevic, Samuel Chassot

We report our experience in enhancing automated grading in a functional programming course using formal verification. In our approach, we deploy a verifier for Scala programs to check equivalences between student submissions and reference solutions. Conseq ...

2024

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

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

New York2022

Proof of Multi-Stage Programming with Generative and Analytical Macros

Martin Odersky, Nicolas Alexander Stucki, Jonathan Immanuel Brachthäuser

In metaprogramming, code generation and code analysis are complementary. Traditionally, principled metaprogramming extensions for programming languages, like MetaML and BER MetaOCaml, offer strong foundations for code generation but lack equivalent support ...

EPFL2021

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

Unifying Analytic and Statically-Typed Quasiquotes

Christoph Koch, Amir Shaikhha, Lionel Emile Vincent Parreaux

Metaprograms are programs that manipulate (generate, analyze and evaluate) other programs. These tasks are greatly facilitated by quasiquotation, a technique to construct and deconstruct program fragments using quoted code templates expressed in the syntax ...

2018

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

Indicators of Evidence for Bioequivalence

Stephan Morgenthaler, Robert Staudte

Some equivalence tests are based on two one-sided tests, where in many applications the test statistics are approximately normal. We define and find evidence for equivalence in Z-tests and then one-and two-sample binomial tests as well as for t-tests. Mult ...

Mdpi Ag2016

Function Passing: A Model for Typed, Distributed Functional Programming

Philipp Haller, Jocelyn Boullier

The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate on which to build data-centric distributed systems. A key id ...

Assoc Computing Machinery2016

Note on the relation between profile scalelengths and lambda's

Olivier Sauter

The calculation of the inverse scalelengths

R/L_T

,

R/L_n

may depend on the choice of the radial variable, depending on the definition of the scalelength. The value of

\lambda_T

and

\lambda_n

, as defined in [O. Sauter {\it et al}, Phys. Plasmas {\bf ...

SPC-EPFL2016

Simply typed lambda calculus

Graph Chatbot

Chat with Graph Search

Formal Autograding in a Classroom (Experience Report)

Degrees of Separation: A Flexible Type System for Safe Concurrency

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

Proof of Multi-Stage Programming with Generative and Analytical Macros

Verified Functional Programming

Unifying Analytic and Statically-Typed Quasiquotes

Implementing Higher-Kinded Types in Dotty

Indicators of Evidence for Bioequivalence

Function Passing: A Model for Typed, Distributed Functional Programming

Note on the relation between profile scalelengths and lambda's

Formal Autograding in a Classroom (Experience Report)

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

Degrees of Separation: A Flexible Type System for Safe Concurrency

Verified Functional Programming

Proof of Multi-Stage Programming with Generative and Analytical Macros

Implementing Higher-Kinded Types in Dotty

Unifying Analytic and Statically-Typed Quasiquotes

Note on the relation between profile scalelengths and lambda's

Indicators of Evidence for Bioequivalence

Function Passing: A Model for Typed, Distributed Functional Programming