Concept
Curry–Howard correspondence
Related publications (5)
When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism
Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki
Type inference in the presence of first-class or "impredicative" second-order polymorphism a la System F has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain ...
Assoc Computing Machinery2024Verified Functional Programming
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 ...
EPFL2019Dotty 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 ...
2017Dependent Object Types
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