EDBT 2026 Demo / reviewers in the wild / expert
Lorenzo Malatesta
dblp:133/3615
· DBLP profile ↗
2ranked-venue papers
0as first author
0since 2021 · last 2013
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 2
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.
| Software engineering, system software, and programming languages
1 paper |
Programming languages and type systems · 100% | |
| Theoretical computer science
1 paper |
Logic in computer science · 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
data types |
0.2 | 1 | 2013 | Fibred Data Types · LICS 2013 |
Programming languages and type systems › type theory › dependent types
indexed types |
0.2 | 1 | 2013 | Fibred Data Types · LICS 2013 |
Programming languages and type systems
type theory |
0.2 | 1 | 2013 | Fibred Data Types · LICS 2013 |
Logic in computer science
category theory |
0.2 | 1 | 2013 | Fibred Data Types · LICS 2013 |
Logic in computer science › category theory
fibration |
0.2 | 1 | 2013 | Fibred Data Types · LICS 2013 |
Methods — techniques the papers use, named apart from their topics
large cardinals · 0.3induction-recursion · 0.3
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2013 | Positive Inductive-Recursive Definitions
Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg |
CALCO | 2 |
| 2013 | Fibred Data TypesabstractData types are undergoing a major leap forward in their sophistication driven by a conjunction of i) theoretical advances in the foundations of data types; and ii) requirements of programmers for ever more control of the data structures they work with. In this paper we develop a theory of indexed data types where, crucially, the indices are generated inductively at the same time as the data. In order to avoid commitment to any specific notion of indexing we take an axiomatic approach to such data types using fibrations - thus giving us a theory of what we call fibred data types. The genesis of these fibred data types can be traced within the literature, most notably to Dybjer and Setzer's introduction of the concept of induction-recursion. This paper, while drawing heavily on their seminal work for inspiration, gives a categorical reformulation of Dybjer and Setzer's original work which leads to a large number of extensions of induction-recursion. Concretely, the paper provides i) conceptual clarity as to what inductionrecursion fundamentally is about; ii) greater expressiveness in allowing not just the inductive-recursive definition of families of sets, or even indexed families of sets, but rather the inductiverecursive definition of a whole host of other structures; iii) a semantics for induction-recursion based not on the specific model of families, but rather an axiomatic model based upon fibrations which therefore encompasses diverse structures (domain theoretic, realisability, games etc) arising in the semantics of programming languages; and iv) technical justification as to why these fibred data types exist using large cardinals from set theory. Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg, Anton Setzer |
LICS | 2 |