Jean-Philippe Bernardy

VLDB 2026 Research / reviewers in the wild / expert

dblp:47/929 · DBLP profile ↗

← Back

28ranked-venue papers

20as first author

7since 2021 · last 2025

0000-0002-8469-5617ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 19 · 16 first-author · 3 since 2021Artificial intelligence and machine learning · 7 · 3 first-author · 3 since 2021Theory of computation · 2 · 2 first-authorSecurity and privacy · 1 · 1 since 2021Databases, data management, data science and information retrieval · 1 · 1 first-authorApplied, interdisciplinary, general and emerging computing · 1 · 1 first-author

Year	Publication	Venue	Position
2025	Domain-specific tensor languages abstract Abstract The tensor notation used in several areas of mathematics is a useful one, but it is not widely available to the functional programming community. In a practical sense, the (embedded) domain-specific languages ( dsl s) that are currently in use for tensor algebra are either 1. array-oriented languages that do not enforce or take advantage of tensor properties and algebraic structure or 2. follow the categorical structure of tensors but require the programmer to manipulate tensors in an unwieldy point-free notation. A deeper issue is that for tensor calculus, the dominant pedagogical paradigm assumes an audience which is either comfortable with notational liberties which programmers cannot afford, or focus on the applied mathematics of tensors, largely leaving their linguistic aspects (behaviour of variable binding, syntax and semantics, etc.) for the reader to figure out by themselves. This state of affairs is hardly surprising, because, as we highlight, several properties of standard tensor notation are somewhat exotic from the perspective of lambda calculi. We bridge the gap by defining a dsl , embedded in Haskell, whose syntax closely captures the index notation for tensors in wide use in the literature. The semantics of this edsl is defined in terms of the algebraic structures which define tensors in their full generality. This way, we believe that our edsl can be used both as a tool for scientific computing, but also as a vehicle to express and present the theory and applications of tensors. Jean-Philippe Bernardy, Patrik Jansson	J. Funct. Program.	1
2024	Algebraic Positional Encodings abstract We introduce a novel positional encoding strategy for Transformer-style models, addressing the shortcomings of existing, often ad hoc, approaches. Our framework implements a flexible mapping from the algebraic specification of a domain to a positional encoding scheme where positions are interpreted as orthogonal operators. This design preserves the structural properties of the source domain, thereby ensuring that the end-model upholds them. The framework can accommodate various structures, including sequences, grids and trees, but also their compositions. We conduct a series of experiments demonstrating the practical applicability of our method. Our results suggest performance on par with or surpassing the current state of the art, without hyper-parameter optimizations or ``task search'' of any kind. Code is available through https://aalto-quml.github.io/ape/. Konstantinos Kogkalidis, Jean-Philippe Bernardy, Vikas Garg 0001	NeurIPS	2
2024	Learning Structure-Aware Representations of Dependent Types abstract Agda is a dependently-typed programming language and a proof assistant, pivotal in proof formalization and programming language theory. This paper extends the Agda ecosystem into machine learning territory, and, vice versa, makes Agda-related resources available to machine learning practitioners. We introduce and release a novel dataset of Agda program-proofs that is elaborate and extensive enough to support various machine learning applications -- the first of its kind. Leveraging the dataset's ultra-high resolution, which details proof states at the sub-type level, we propose a novel neural architecture targeted at faithfully representing dependently-typed programs on the basis of structural rather than nominal principles. We instantiate and evaluate our architecture in a premise selection setup, where it achieves promising initial results, surpassing strong baselines. Konstantinos Kogkalidis, Orestis Melkonian, Jean-Philippe Bernardy	NeurIPS	3
2022	UniMorph 4.0: Universal Morphology abstract The Universal Morphology (UniMorph) project is a collaborative effort providing broad-coverage instantiated normalized morphological inflection tables for hundreds of diverse world languages. The project comprises two major thrusts: a language-independent feature schema for rich morphological annotation, and a type-level resource of annotated data in diverse languages realizing that schema. This paper presents the expansions and improvements on several fronts that were made in the last couple of years (since McCarthy et al. (2020)). Collaborative efforts by numerous linguists have added 66 new languages, including 24 endangered languages. We have implemented several improvements to the extraction pipeline to tackle some issues, e.g., missing gender and macrons information. We have amended the schema to use a hierarchical structure that is needed for morphological phenomena like multiple-argument agreement and case stacking, while adding some missing morphological features to make the schema more inclusive. In light of the last UniMorph release, we also augmented the database with morpheme segmentation for 16 languages. Lastly, this new release makes a push towards inclusion of derivational morphology in UniMorph by enriching the data and annotation schema with instances representing derivational processes from MorphyNet. Khuyagbaatar Batsuren, Omer Goldman, Salam Khalifa, Nizar Habash, Witold Kieras, Gábor Bella, Brian Leonard, Garrett Nicolai, Kyle Gorman, Yustinus Ghanggo Ate, Maria Ryskina, Sabrina J. Mielke, Elena Budianskaya, Charbel El-Khaissi, Tiago Pimentel, Michael Gasser, William Lane 0002, Mohit Raj, Matt Coler, Jaime Rafael Montoya Samame, Delio Siticonatzi Camaiteri, Esaú Zumaeta Rojas, Didier López Francis, Arturo Oncevay, Juan López Bautista, Gema Celeste Silva Villegas, Lucas Torroba Hennigen, Adam Ek, David Guriel, Peter Dirix, Jean-Philippe Bernardy, Andrey Scherbakov, Aziyana Bayyr-ool, Antonios Anastasopoulos, Roberto Zariquiey, Karina Sheifer, Sofya Ganieva, Hilaria Cruz, Ritván Karahóga, Stella Markantonatou, George Pavlidis, Matvey Plugaryov, Elena Klyachko, Ali Salehi, Candy Angulo, Jatayu Baxi, Andrew Krizhanovsky, Natalia Krizhanovskaya, Elizabeth Salesky, Clara Vania, Sardana Ivanova, Jennifer C. White, Rowan Hall Maudslay, Josef Valvoda, Ran Zmigrod, Paula Czarnowska, Irene Nikkarinen, Aelita Salchak, Brijesh Bhatt, Christopher Straughn, Zoey Liu, Jonathan Washington, Yuval Pinter, Duygu Ataman, Marcin Wolinski, Totok Suhardijanto, Anna Yablonskaya, Niklas Stoehr, Hossep Dolatian, Zahroh Nuriah, Shyam Ratan, Francis M. Tyers, Edoardo Maria Ponti, Grant Aiton, Aryaman Arora, Richard J. Hatcher, Ritesh Kumar 0002, Jeremiah Young, Daria Rodionova, Anastasia Yemelina, Taras Andrushko, Igor Marchenko, Polina Mashkovtseva, Alexandra Serova, Emily Tucker Prud'hommeaux, Maria Nepomniashchaya, Fausto Giunchiglia, Eleanor Chodroff, Mans Hulden, Miikka Silfverberg, Arya McCarthy, David Yarowsky, Ryan Cotterell, Reut Tsarfaty, Ekaterina Vylomova	LREC	31
2022	Linearly qualified types: generic inference for capabilities and uniqueness abstract A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used safely. However, writing code with explicit linear arguments requires bureaucracy. This paper presents linear constraints, a front-end feature for linear typing that decreases the bureaucracy of working with linear types. Linear constraints are implicit linear arguments that are filled in automatically by the compiler. We present linear constraints as a qualified type system,together with an inference algorithm which extends GHC's existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell. Arnaud Spiwack, Csongor Kiss, Jean-Philippe Bernardy, Nicolas Wu, Richard A. Eisenberg	Proc. ACM Program. Lang.	3
2021	Dynamic IFC Theorems for Free! abstract We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained “for free”, as direct consequences of the more general parametricity theorem of type abstraction. This allows us to give very short soundness proofs for dynamic IFC libraries such as faceted values and LIO. Our proofs stay short even when fully mechanized for Agda implementations of the libraries in terms of type abstraction. Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu	CSF	2
2021	Evaluating linear functions to symmetric monoidal categories abstract A number of domain specific languages, such as circuits or data-science workflows, are best expressed as diagrams of boxes connected by wires. Unfortunately, functional languages have traditionally been ill-equipped to embed this sort of languages. The Arrow abstraction is an approximation, but we argue that it does not capture the right properties. Jean-Philippe Bernardy, Arnaud Spiwack	Haskell	1
2020	Identifying Sentiments in Algerian Code-switched User-generated Comments abstract We present in this paper our work on Algerian language, an under-resourced North African colloquial Arabic variety, for which we built a comparably large corpus of more than 36,000 code-switched user-generated comments annotated for sentiments. We opted for this data domain because Algerian is a colloquial language with no existing freely available corpora. Moreover, we compiled sentiment lexicons of positive and negative unigrams and bigrams reflecting the code-switches present in the language. We compare the performance of four models on the task of identifying sentiments, and the results indicate that a CNN model trained end-to-end fits better our unedited code-switched and unbalanced data across the predefined sentiment classes. Additionally, injecting the lexicons as background knowledge to the model boosts its performance on the minority class with a gain of 10.54 points on the F-score. The results of our experiments can be used as a baseline for future research for Algerian sentiment analysis. Wafia Adouane, Samia Touileb, Jean-Philippe Bernardy	LREC	3
2020	Improving the Precision of Natural Textual Entailment Problem Datasets abstract In this paper, we propose a method to modify natural textual entailment problem datasets so that they better reflect a more precise notion of entailment. We apply this method to a subset of the Recognizing Textual Entailment datasets. We thus obtain a new corpus of entailment problems, which has the following three characteristics: 1. it is precise (does not leave out implicit hypotheses) 2. it is based on “real-world” texts (i.e. most of the premises were written for purposes other than testing textual entailment). 3. its size is 150. Broadly, the method that we employ is to make any missing hypotheses explicit using a crowd of experts. We discuss the relevance of our method in improving existing NLI datasets to be more fit for precise reasoning and we argue that this corpus can be the basis a first step towards wide-coverage testing of precise natural-language inference systems. Jean-Philippe Bernardy, Stergios Chatzikyriakidis	LREC	1
2020	A unified view of modalities in type systems abstract We propose to unify the treatment of a broad range of modalities in typed lambda calculi. We do so by defining a generic structure of modalities, and show that this structure arises naturally from the structure of intuitionistic logic, and as such finds instances in a wide range of type systems previously described in literature. Despite this generality, this structure has a rich metatheory, which we expose. Andreas Abel 0001, Jean-Philippe Bernardy	Proc. ACM Program. Lang.	2
2019	What Kind of Natural Language Inference are NLP Systems Learning: Is this Enough? abstract In this paper, we look at Natural Language Inference, arguing that the notion of inference the current NLP systems are learning is much narrower compared to the range of inference patterns found in human reasoning. We take a look at the history and the nature of creating datasets for NLI. We discuss the datasets that are mainly used today for the relevant tasks and show why those are not enough to generalize to other reasoning tasks, e.g. logical and legal reasoning, or reasoning in dialogue settings. We then proceed to propose ways in which this can be remedied, effectively producing more realistic datasets for NLI. Lastly, we argue that the NLP community could have been too hasty to altogether dismiss symbolic approaches in the study of NLI, given that these might still be relevant for more fine-grained cases of reasoning. As such, we argue for a more pluralistic take on tackling NLI, favoring hybrid rather than non-hybrid approaches. Jean-Philippe Bernardy, Stergios Chatzikyriakidis	ICAART (2)	1
2019	Two experiments for embedding Wordnet hierarchy into vector spaces abstract In this paper, we investigate mapping of the WORDNET hyponymy relation to feature vectors.Our aim is to model lexical knowledge in such a way that it can be used as input in generic machine-learning models, such as phrase entailment predictors.We propose two models.The first one leverages an existing mapping of words to feature vectors (fastText), and attempts to classify such vectors as within or outside of each class.The second model is fully supervised, using solely WORDNET as a ground truth.It maps each concept to an interval or a disjunction thereof.The first model approaches but not quite attain state of the art performance.The second model can achieve near-perfect accuracy. Jean-Philippe Bernardy, Aleksandre Maskharashvili	GWC	1
2019	Simple noninterference from parametricity abstract In this paper we revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a polyvariant variation of the Dependency Core Calculus of in the Calculus of Constructions. The proof is modular: it leverages parametricity for the Calculus of Constructions and the encoding of data abstraction using existential types. This perspective gives rise to simple and understandable proofs of noninterference from parametricity. All our contributions have been mechanised in the Agda proof assistant. Maximilian Algehed, Jean-Philippe Bernardy	Proc. ACM Program. Lang.	2
2018	Linear Haskell: practical linearity in a higher-order polymorphic language abstract Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility and code reuse across linear and non-linear users of a library. Only then can the benefits of linear types permeate conventional functional programming. Rather than bifurcate types into linear and non-linear counterparts, we instead attach linearity to function arrows . Linear functions can receive inputs from linearly-bound values, but can also operate over unrestricted, regular values. To demonstrate the efficacy of our linear type system — both how easy it can be integrated in an existing language implementation and how streamlined it makes it to write programs with linear types — we implemented our type system in ghc, the leading Haskell compiler, and demonstrate two kinds of applications of linear types: mutable data with pure interfaces; and enforcing protocols in I/O-performing functions. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan Newton, Simon L. Peyton Jones, Arnaud Spiwack	Proc. ACM Program. Lang.	1
2017	A pretty but not greedy printer (functional pearl) abstract This paper proposes a new specification of pretty printing which is stronger than the state of the art: we require the output to be the shortest possible, and we also offer the ability to align sub-documents at will. We argue that our specification precludes a greedy implementation. Yet, we provide an implementation which behaves linearly in the size of the output. The derivation of the implementation demonstrates functional programming methodology. Jean-Philippe Bernardy	Proc. ACM Program. Lang.	1
2015	Efficient parallel and incremental parsing of practical context-free languages abstract Abstract We present a divide-and-conquer algorithm for parsing context-free languages efficiently. Our algorithm is an instance of Valiant's (1975; General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10 (2), 308–314), who reduced the problem of parsing to matrix multiplications. We show that, while the conquer step of Valiant's is O ( n 3 ), it improves to O (log 2 n ) under certain conditions satisfied by many useful inputs that occur in practice, and if one uses a sparse representation of matrices. The improvement happens because the multiplications involve an overwhelming majority of empty matrices. This result is relevant to modern computing: divide-and-conquer algorithms with a polylogarithmic conquer step can be parallelized relatively easily. Jean-Philippe Bernardy, Koen Claessen	J. Funct. Program.	1
2013	Names for free: polymorphic views of names and binders abstract We propose a novel technique to represent names and binders in Haskell. The dynamic (run-time) representation is based on de Bruijn indices, but it features an interface to write and manipulate variables conviently, using Haskell-level lambdas and variables. The key idea is to use rich types: a subterm with an additional free variable is viewed either as forallν.ν → Term(ɑ + ν) or ϶ν.ν x Term(ν.ν) depending on whether it is constructed or analysed. We demonstrate on a number of examples how this approach permits to express term construction and manipulation in a natural way, while retaining the good properties of representations based on de Bruijn indices. Jean-Philippe Bernardy, Nicolas Pouillard	Haskell	1
2013	Efficient divide-and-conquer parsing of practical context-free languages abstract We present a divide-and-conquer algorithm for parsing context-free languages efficiently. Our algorithm is an instance of Valiant's (1975), who reduced the problem of parsing to matrix multiplications. We show that, while the conquer step of Valiant's is O(n3) in the worst case, it improves to O(logn3), under certain conditions satisfied by many useful inputs. These conditions occur for example in program texts written by humans. The improvement happens because the multiplications involve an overwhelming majority of empty matrices. This result is relevant to modern computing: divide-and-conquer algorithms can be parallelized relatively easily. Jean-Philippe Bernardy, Koen Claessen	ICFP	1
2013	Type-theory in color abstract Dependent type-theory aims to become the standard way to formalize mathematics at the same time as displacing traditional platforms for high-assurance programming. However, current implementations of type theory are still lacking, in the sense that some obvious truths require explicit proofs, making type-theory awkward to use for many applications, both in formalization and programming. In particular, notions of erasure are poorly supported. Jean-Philippe Bernardy, Guilhem Moulin	ICFP	1
2012	A Computational Interpretation of Parametricity abstract Reynolds' abstraction theorem has recently been extended to lambda-calculi with dependent types. In this paper, we show how this theorem can be internalized. More precisely, we describe an extension of the Pure Type Systems with a special parametricity rule (with computational content), and prove fundamental properties such as Church-Rosser's and strong normalization. All instances of the abstraction theorem can be both expressed and proved in the calculus itself. Moreover, one can apply parametricity to the parametricity rule: parametricity is itself parametric. Jean-Philippe Bernardy, Guilhem Moulin	LICS	1
2012	Proofs for free - Parametricity for dependent types abstract Abstract Reynolds' abstraction theorem (Reynolds, J. C. (1983) Types, abstraction and parametric polymorphism, Inf. Process. 83 (1), 513–523) shows how a typing judgement in System F can be translated into a relational statement (in second-order predicate logic) about inhabitants of the type. We obtain a similar result for pure type systems (PTSs): for any PTS used as a programming language, there is a PTS that can be used as a logic for parametricity. Types in the source PTS are translated to relations (expressed as types) in the target. Similarly, values of a given type are translated to proofs that the values satisfy the relational interpretation. We extend the result to inductive families. We also show that the assumption that every term satisfies the parametricity condition generated by its type is consistent with the generated logic. Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson	J. Funct. Program.	1
2011	Realizability and Parametricity in Pure Type Systems Jean-Philippe Bernardy, Marc Lasson	FoSSaCS	1
2010	Testing Polymorphic Properties Jean-Philippe Bernardy, Patrik Jansson, Koen Claessen	ESOP	1
2010	Parametricity and dependent types abstract Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into a relational statement (in second order predicate logic) about inhabitants of the type. We (in second order predicate logic) about inhabitants of the type. We obtain a similar result for a single lambda calculus (a pure type system), in which terms, types and their relations are expressed. Working within a single system dispenses with the need for an interpretation layer, allowing for an unusually simple presentation. While the unification puts some constraints on the type system (which we spell out), the result applies to many interesting cases, including dependently-typed ones. Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson	ICFP	1
2010	Generic programming with C++ concepts and Haskell type classes - a comparison abstract Abstract Earlier studies have introduced a list of high-level evaluation criteria to assess how well a language supports generic programming. Languages that meet all criteria include Haskell because of its type classes and C++ with the concept feature. We refine these criteria into a taxonomy that captures commonalities and differences between type classes in Haskell and concepts in C++ and discuss which differences are incidental and which ones are due to other language features. The taxonomy allows for an improved understanding of language support for generic programming, and the comparison is useful for the ongoing discussions among language designers and users of both languages. Jean-Philippe Bernardy, Patrik Jansson, Marcin Zalewski, Sibylle Schupp	J. Funct. Program.	1
2009	Lazy functional incremental parsing abstract Structured documents are commonly edited using a free-form editor. Even though every string is an acceptable input, it makes sense to maintain a structured representation of the edited document. The structured representation has a number of uses: structural navigation (and optional structural editing), structure highlighting, etc. The construction of the structure must be done incrementally to be efficient: the time to process an edit operation should be proportional to the size of the change, and (ideally) independent of the total size of the document. We show that combining lazy evaluation and caching of intermediate (partial) results enables incremental parsing. We build a complete incremental parsing library for interactive systems with support for error-correction. Jean-Philippe Bernardy	Haskell	1
2008	Yi: an editor in haskell for haskell abstract Yi is a text editor written in Haskell and extensible in Haskell. We take advantage of Haskell's expressive power to define embedded DSLs that form the foundation of the editor. In turn, these DSLs provide a flexible mechanism to create extended versions of the editor. Yi also provides some support for editing Haskell code. Jean-Philippe Bernardy	Haskell	1
2002	Reviving Pacbase COBOL-Generated Code abstract We have migrated a large scale application from Pacbase to COBOL. The technique applies, in an iterative fashion, a set of small transformation patterns on Pacbase COBOL-output. Thus, equivalence with the Pacbase code is easily verified. Jean-Philippe Bernardy	COMPSAC	1