EDBT 2026 Demo / reviewers in the wild / expert
Yorgo Chamoun
dblp:352/2599
· DBLP profile ↗
2ranked-venue papers
1as first author
2since 2021 · last 2026
0009-0007-2689-9148ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 2 · 1 first-author · 2 since 2021Theory of computation · 1 · 1 first-author · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
1 paper |
Logic in computer science · 100% | |
| Software engineering, system software, and programming languages
1 paper |
Programming languages and type systems · 100% |
Topics — the 5 heaviest of 5, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Programming languages and type systems
type theory |
0.8 | 1 | 2024 | Internal Parametricity, without an Interval · Proc. ACM Program. Lang. 2024 |
Logic in computer science
categorical semantics |
0.8 | 1 | 2024 | Internal Parametricity, without an Interval · Proc. ACM Program. Lang. 2024 |
Logic in computer science › categorical semantics
presheaf model |
0.8 | 1 | 2024 | Internal Parametricity, without an Interval · Proc. ACM Program. Lang. 2024 |
Programming languages and type systems › type theory › dependent types
martin-löf type theory |
0.2 | 1 | 2024 | Internal Parametricity, without an Interval · Proc. ACM Program. Lang. 2024 |
Programming languages and type systems › type theory
modal type theory |
0.2 | 1 | 2024 | Internal Parametricity, without an Interval · Proc. ACM Program. Lang. 2024 |
Methods — techniques the papers use, named apart from their topics
span-based parametricity · 1.5presheaf model · 1.5gluing · 1.5
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Realization of Relational Presheaves
Yorgo Chamoun, Samuel Mimram |
FoSSaCS | 1 |
| 2024 | Internal Parametricity, without an IntervalabstractParametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it is difficult because once there is a term witnessing parametricity, it also has to be parametric itself and this results in the appearance of higher dimensional cubes. In previous theories with internal parametricity, either an explicit syntax for higher cubes is present or the theory is extended with a new sort for the interval. In this paper we present a type theory with internal parametricity which is a simple extension of Martin-Löf type theory: there are a few new type formers, term formers and equations. Geometry is not explicit in this syntax, but emergent: the new operations and equations only refer to objects up to dimension 3. We show that this theory is modelled by presheaves over the BCH cube category. Fibrancy conditions are not needed because we use span-based rather than relational parametricity. We define a gluing model for this theory implying that external parametricity and canonicity hold. The theory can be seen as a special case of a new kind of modal type theory, and it is the simplest setting in which the computational properties of higher observational type theory can be demonstrated. Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman |
Proc. ACM Program. Lang. | 2 |