Heben Sie Ihre Leistungen auf People@HES-SO hervor weitere Infos
PEOPLE@HES-SO - Verzeichnis der Mitarbeitenden und Kompetenzen
PEOPLE@HES-SO - Verzeichnis der Mitarbeitenden und Kompetenzen

PEOPLE@HES-SO
Verzeichnis der Mitarbeitenden und Kompetenzen

Hilfe
language
  • fr
  • en
  • de
  • fr
  • en
  • de
  • SWITCH edu-ID
  • Verwaltung
ID
« Zurück
Racordon Dimi

Racordon Dimi

Professeur-e HES Assistant-e

Hauptkompetenzen

Développement logiciel

Construction de compilateurs

Systèmes d'exploitation

Méthodes formelles

  • Kontakt

  • Lehre

  • Publikationen

  • Portfolio

Hauptvertrag

Professeur-e HES Assistant-e

Büro: ENP.23.N317

HES-SO Valais-Wallis - Haute Ecole d'Ingénierie
Rue de l'Industrie 23, 1950 Sion, CH
HEI - VS
Bereich
Technique et IT
Hauptstudiengang
Informatique et systèmes de communication
MSc HES-SO en Engineering - HES-SO Master
  • Programmation avancée
BSC HES-SO en Informatique et systèmes de communication - HES-SO Valais-Wallis - Haute Ecole d'Ingénierie
  • Systèmes d'exploitation
  • Programmation fonctionnelle
  • Software engineering

2025

Who Owns the Contents of a Doubly-Linked List?
Wissenschaftlicher Artikel

Racordon Dimi

Companion Proceedings of the 9th International Conference on the Art, Science, and Engineering of Programming, 2025

Link zur Publikation

Zusammenfassung:

Despite their popularity, systems enforcing full ownership guarantees such as Rust leave many users frustrated with the inability to represent notionally self-referential data structures - e.g., doubly-linked lists - using first-class references. This frustration has motivated a number of proposals to relax on full ownership to support idioms common in languages with pervasive reference semantics. In this paper, we take a look at the way value-oriented languages address this issue and study representations of arbitrary graph-like data structures without references.

Use Site Checking Considered Harmful
Wissenschaftlicher Artikel

Racordon Dimi, Chung Benjamin

Onward! 2024: Proceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, 2025

Link zur Publikation

Zusammenfassung:

Static type checking aims to detect nonsensical operations based on their domains at compile time. While its benefits no longer need to be argued, it comes with expressiveness limitations that can only be lifted at the expense of complexity. This problem is particularly antithetical to generic programming, where algorithms and data structures are designed in the most general setting possible. In response, some systems have adopted a form of static duck typing: generic definitions are written against assumed interfaces that are only type checked with concrete types at their ultimate use sites. This essay claims that such an approach, which we refer to as use site checking, is harmful to user experience. We study four main problems caused by use site checking and show how they relate to similar well-known issues in dynamically typed languages. We then look at existing language constructs to discuss how statically typed languages may address these shortcomings.

Existentialize Your Generics
Wissenschaftlicher Artikel

Racordon Dimi, Bovel Matt, Remmal Hamza

Proceedings of the 22nd ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes, 2025

Link zur Publikation

Zusammenfassung:

The two main approaches to compile generic programs are dynamic dispatch and monomorphization. While the latter is typically preferred in the context of low latency applications, where the overhead of boxing may be prohibitive, it also comes at the cost of important limitations in terms of modularity, expressiveness, and code size. 

The Swift programming language proposes an interesting third alternative that addresses these shortcomings, supporting dynamic dispatch without requiring boxing by factoring method tables out of object headers. This paper examines the merits of that strategy, which we call existentialization, across different programming languages. Our study shows that existentialization can produce code with competitive performance with respect to monomorphization.

On the State of Coherence in the Land of Type Classes
Wissenschaftlicher Artikel

Racordon Dimi, Flesselle Eugène, Pham Cao Nguyen

The Art, Science, and Engineering of Programming, 2025 , vol.  10, no  1

Link zur Publikation

Zusammenfassung:

Type classes are a popular tool for implementing generic algorithms and data structures without loss of efficiency, bridging the gap between parametric and ad-hoc polymorphism. Since their initial development in Haskell, they now feature prominently in numerous other industry-ready programming languages, notably including Swift, Rust, and Scala. The success of type classes hinges in large part on the compilers’ ability to infer arguments to implicit parameters by means of a type-directed resolution. This technique, sometimes dubbed implicit programming, lets users elide information that the language implementation can deduce from the context, such as the implementation of a particular type class.

One drawback of implicit programming is that a type-directed resolution may yield ambiguous results, thereby threatening coherence, the property that valid programs have exactly one meaning. This issue has divided the community on the right approach to address it. One side advocates for flexibility where implicit resolution is context-sensitive and often relies on dependent typing features to uphold soundness. The other holds that context should not stand in the way of equational reasoning and typically imposes that type class instances be unique across the entire program to fend off ambiguities.

Although there exists a large body of work on type classes and implicit programming, most of the scholarly literature focuses on a few select languages and offers little insight into other mainstream projects. Meanwhile, the latter have evolved similar features and/or restrictions under different names, making it difficult for language users and designers to get a sense of the full design space. To alleviate this issue, we set to examine Swift, Rust, and Scala, three popular languages featuring type classes heavily, and relate their approach to coherence to Haskell’s. It turns out that, beyond superficial syntactic differences, Swift, Rust, and Haskell are actually strikingly similar in that the three languages offer comparable strategies to work around the limitations of the uniqueness of type class instances.

2024

Existential Containers in Scala
Wissenschaftlicher Artikel

Racordon Dimi, Flesselle Eugène, Bovel Matt

MPLR 2024: Proceedings of the 21st ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes, 2024

Link zur Publikation

Zusammenfassung:

Type classes have been well-established as a powerful tool to write generic algorithms and data structures while escaping vexing limitations of subtyping with respect to extensibility, binary methods, and partial abstractions. Unfortunately, type classes are typically inadequate to express run-time polymorphism and dynamic dispatch, two features considered central to object-oriented systems. This paper explains how to alleviate this problem in Scala. We present existential containers, a form of existential types bounded by type classes rather than types, and explain how to implement them using Scala’s existing features.

Type Checking with Rewriting Rules
Wissenschaftlicher Artikel

Racordon Dimi

SLE 2024: Proceedings of the 17th ACM SIGPLAN International Conference on Software Language Engineering, 2024

Link zur Publikation

Zusammenfassung:

Type classes support the implementation of highly reusable algorithms and data structures without loss of efficiency. Initially developed in Haskell, they have become central to the design of several modern programming languages, including Swift, Rust, Hylo, and Carbon. A key part of their success is the ability to express sophisticated abstractions using constraints on the types associated with their operations. However, this expressiveness invites thorny theoretical and engineering questions. In particular, the support of recursive constraints—i.e., constraints specifying that an associated type of an abstraction must be a model of that abstraction—leaves type equivalence undecidable. This paper studies a semi-decidable technique to tackle this problem that was first developed in Swift’s compiler. The core idea is to encode constraints into a term rewriting system and use normalization to answer type checking queries. We describe this approach formally through the lens of, a calculus originally designed to capture generic programming best practices; and discuss an implementation in the context of Hylo, a language inspired by Swift and Rust.

Method Bundles
Wissenschaftlicher Artikel

Racordon Dimi, Abrahams Dave

SLE 2024: Proceedings of the 17th ACM SIGPLAN International Conference on Software Language Engineering, 2024

Link zur Publikation

Zusammenfassung:

Performance-critical systems commonly optimize memory use and locality by selecting among multiple variants of a single logical operation. Algorithm developers then typically rely on ad-hoc API patterns or naming conventions to distinguish the variants. Unfortunately, this practice suffers from poor ergonomics. Users are compelled to understand the conventions and carefully consider the signatures and documentation of different variants, which creates drag on development and maintenance. Instead, we propose a language construct bundling algorithm variants having well-defined semantic relationships under a single name. This approach eliminates boilerplate, reduces cognitive overhead by consolidating APIs, and unlocks compiler optimizations.

2023

Borrow Checking Hylo
Wissenschaftlicher Artikel

Racordon Dimi, Abrahams Dave

IWACO 2023, 2023

Link zur Publikation

Zusammenfassung:

Hylo is a language for high-level systems programming that promises safety without loss of efficiency. It is based on mutable value semantics, a discipline that emphasizes the independence of values to support local reasoning. The result—in contrast with approaches based on sophisticated aliasing restrictions—is an efficient, expressive language with a simple type system and no need for lifetime annotations.

Safety guarantees in Hylo programs are verified by an abstract interpreter processing an intermediate representation, Hylo IR, that models lifetime properties with ghost instructions. Further, lifetime constraints are used to eliminate unnecessary memory allocations predictably.

2022

Implementation Strategies for Mutable Value Semantics.
Wissenschaftlicher Artikel

Racordon Dimi, Shabalin Denys, Zheng Daniel, Abrahams Dave, Saeta Brennan

Journal of Object Technology, 2022

Link zur Publikation

Zusammenfassung:

Mutable value semantics is a programming discipline that upholds the independence of values to support local reasoning. In the discipline’s strictest form, references become second-class citizens: they are only created implicitly, at function boundaries, and cannot be stored in variables or object fields. Hence, variables can never share mutable state. Unlike pure functional programming, however, mutable value semantics allows part-wise in-place mutation, thereby eliminating the memory traffic usually associated with functional updates of immutable data. This paper presents implementation strategies for compiling programs with mutable value semantics into efficient native code. We study Swift, a programming language based on that discipline, through the lens of a core language that strips some of Swift’s features to focus on the semantics of its value types. The strategies that we introduce leverage the inherent properties of mutable value semantics to unlock aggressive optimizations. Fixed-size values are allocated on the stack, thereby enabling numerous off-the-shelf compiler optimizations, while dynamically sized containers use copy-on-write to mitigate copying costs.

2020

Featherweight Swift: a Core calculus for Swift’s type system
Wissenschaftlicher Artikel

Racordon Dimi, Buchs Didier

SLE 2020: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering, 2020

Link zur Publikation

Zusammenfassung:

Swift is a modern general-purpose programming language, designed to be a replacement for C-based languages. Although primarily directed at development of applications for Apple's operating systems, Swift's adoption has been growing steadily in other domains, ranging from server-side services to machine learning. This success can be partly attributed to a rich type system that enables the design of safe, fast, and expressive programming interfaces. Unfortunately, this richness comes at the cost of complexity, setting a high entry barrier to exploit Swift's full potential. Furthermore, existing documentation typically only relies on examples, leaving new users with little help to build a deeper understanding of the underlying rules and mechanisms.

This paper aims to tackle this issue by laying out the foundations for a formal framework to reason about Swift's type system. We introduce Featherweight Swift, a minimal language stripped of all features not essential to describe its typing rules. Featherweight Swift features classes and protocol inheritance, supports retroactive modeling, and emulates Swift's overriding mechanisms. Yet its formalization fits on a few pages. We present Featherweight Swift's syntax and semantics. We then elaborate on the usability of our framework to reason about Swift's features, future extensions, and implementation by discussing a bug in Swift's compiler, discovered throughout the design of our calculus.

Errungenschaften

Sans date

Hylo – A programming language for high-level systems programming

 2026 ; Open Source Project

Collaborateurs: Racordon Dimi

Link zur Errungenschaft

Hylo is a programming language that leverages mutable value semantics and generic programming for high-level systems programming.

Hylo aims to be:

  • Fast by definition: Hylo is compiled ahead-of-time to machine code and relies on its type system to support in-place mutation and avoid unnecessary memory allocations. Hylo avoids hidden costs such as implicit copies and therefore avoids heavy dependence on an optimizer for basic performance.
  • Safe by default: Hylo’s foundation of mutable value semantics ensures that ordinary code is memory safe, typesafe, and data-race-free. By explicit, auditable opt-in, programmers can use unsafe constructs for performance where necessary, and can build safe constructs using unsafe ones.
  • Simple: Hylo borrows heavily from Swift which has demonstrated a user-friendly approach to generic programming and deep support for value semantics. Hylo’s programming model strengthens and extends this support, while de-emphasizing reference semantics and avoiding the complexities that result from trying to make it statically safe (e.g., memory regions, lifetime annotations, etc.).

Medien und Kommunikation
Kontaktieren Sie uns
Folgen Sie der HES-SO
linkedin instagram facebook twitter youtube rss
univ-unita.eu www.eua.be swissuniversities.ch
Rechtliche Hinweise
© 2021 - HES-SO.

HES-SO Rectorat