Demo Data from EDBT 2026 / reviewers in the wild / expert
Nax Paul Mendler
dblp:46/3262
· DBLP profile ↗
4ranked-venue papers
4as first author
0since 2021 · last 1991
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 4 · 4 first-author
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
3 papers |
Programming languages and type systems · 100% |
Topics — the 5 heaviest of 6, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Programming languages and type systems › type theory
inductive types |
0.0 | 1 | 1991 | Predicative Type Universes and Primitive Recursion · LICS 1991 |
Programming languages and type systems › lambda calculus
polymorphic lambda calculus |
0.0 | 1 | 1987 | Recursive Types and Type Constraints in Second-Order Lambda Calculus · LICS 1987 |
Programming languages and type systems › type systems
recursive types |
0.0 | 1 | 1987 | Recursive Types and Type Constraints in Second-Order Lambda Calculus · LICS 1987 |
Programming languages and type systems › type systems
type constraints |
0.0 | 1 | 1987 | Recursive Types and Type Constraints in Second-Order Lambda Calculus · LICS 1987 |
Programming languages and type systems
type theory |
0.0 | 1 | 1986 | Infinite Objects in Type Theory · LICS 1986 |
Methods — techniques the papers use, named apart from their topics
universe hierarchies · 0.0i-algebra · 0.0categories with display maps · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 1991 | Predicative Type Universes and Primitive RecursionabstractA category-theoretic explanation of predicative type universes and primitive recursion on them is given. Categories with display maps (cdm) (with canonical pullbacks) are used to model families. A slight generalization of an algebra, called an I-algebra, is given. Primitive recursion is defined, and the general definition of primitive recursion on a cdm which can justify the elimination rules for all the usual inductively defined datatypes, including universes, as an instance, is given. It is shown how operations may be reflected, allowing an I-algebra to be closed under type-forming operations. Universe hierarchies are built: an externally constructed one, and then a large type universe, itself closed under universe construction, in which universe hierarchies can be internally constructed. As an example, a hierarchy up to omega is constructed.> Nax Paul Mendler |
LICS | 1 |
| 1991 | Inductive Types and Type Constraints in the Second-Order lambda Calculus
Nax Paul Mendler |
Ann. Pure Appl. Log. | 1 |
| 1987 | Recursive Types and Type Constraints in Second-Order Lambda Calculus
Nax Paul Mendler |
LICS | 1 |
| 1986 | Infinite Objects in Type Theory
Nax Paul Mendler, Prakash Panangaden, Robert L. Constable |
LICS | 1 |