Publications related to Subtyping

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 Machinery2024

Formal Foundations of Capture Tracking

Aleksander Slawomir Boruch-Gruszecki

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

Type-Preserving Compilation of Class-Based Languages

Guillaume André Fradji Martres

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is ...

EPFL2023

DFT plus U-type functional derived to explicitly address the flat plane condition

Edward Baxter Linscott

A DFT+U-type corrective functional is derived from first principles to enforce the flat plane condition on localized subspaces, thus dispensing with the need for an ad hoc derivation from the Hubbard model. Small, molecular test systems at the dissociated ...

AMER PHYSICAL SOC2023

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

Type-preserving compilation of (most of) FGJ into DOT

Guillaume André Fradji Martres

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not e ...

2022

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

ASSOC COMPUTING MACHINERY2022

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain, Jonathan Immanuel Brachthäuser

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents \emph{match ...

2021

FTLD-TDP assemblies seed neoaggregates with subtype-specific features via a prion-like cascade

Henning Paul-Julius Stahlberg, Amanda Jennifer Lewis, Marta Di Fabrizio, Julien Weber

Morphologically distinct TDP-43 aggregates occur in clinically different FTLD-TDP subtypes, yet the mechanism of their emergence and contribution to clinical heterogeneity are poorly understood. Several lines of evidence suggest that pathological TDP-43 fo ...

WILEY2021

Type Soundness Proofs with Definitional Interpreters

Tiark Rompf, Nada Amin

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculu ...

Assoc Computing Machinery2017

Subtyping

When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism

Formal Foundations of Capture Tracking

Type-Preserving Compilation of Class-Based Languages

DFT plus U-type functional derived to explicitly address the flat plane condition

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

Type-preserving compilation of (most of) FGJ into DOT

Type-Level Programming with Match Types

Type-Level Programming with Match Types

FTLD-TDP assemblies seed neoaggregates with subtype-specific features via a prion-like cascade

Type Soundness Proofs with Definitional Interpreters

Graph Chatbot

Chat with Graph Search

Type-Preserving Compilation of Class-Based Languages

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

Type-Level Programming with Match Types

Type Soundness Proofs with Definitional Interpreters

When Subtyping Constraints Liberate A Novel Type Inference Approach for First-Class Polymorphism

DFT plus U-type functional derived to explicitly address the flat plane condition

Type-Level Programming with Match Types

Formal Foundations of Capture Tracking

Type-preserving compilation of (most of) FGJ into DOT

FTLD-TDP assemblies seed neoaggregates with subtype-specific features via a prion-like cascade