2.1 Objectives

The project-team investigates the design of logical frameworks, in order to ensure interoperability between proof systems, and to the development of system-independent proof libraries. To achieve these goals, we develop

• a logical framework Dedukti, where several theories can be expressed,
• tools to import proofs developed in external proof systems to Dedukti theories,
• tools to translate proofs from one Dedukti theory to another,
• tools to export proofs expressed in Dedukti theories to an external proof system,
• tools to prove the confluence, the termination, and the consistency of theories expressed in Dedukti,
• tools to develop proofs directly in Dedukti,
• an encyclopedia Logipedia of proofs expressed in various Dedukti theories.

2.2 History

The idea that systems such as Euclidean geometry or set theory should be expressed, not as independent systems, but in a logical framework appeared with the design of the first logical framework: predicate logic, in 1928. Later, several more powerful logical frameworks have been designed: $\lambda$-prolog, Isabelle, the Edinburgh logical framework, Pure type systems, and Deduction modulo theory.

The logical framework that we use is a simple $\lambda$-calculus with dependent types and rewrite rules, called the $\lambda \Pi$-calculus modulo theory, and also the Martin-Löf logical framework, and it generalizes all the mentioned frameworks. It is implemented in the system Dedukti.

The first version of Dedukti was developed in 2011 by Mathieu Boespflug 35. From 2012 to 2015, new versions of Dedukti were developed and several theories were expressed in Dedukti, allowing to import proofs developed in Matita (with the tool Krajono), HOL Light (with the tool Holide), FoCaLiZe (with the tool Focalide), iProver, and Zenon, totalizing several hundred of megabytes of proofs. The development of Dedukti has now been completed.

We now focus on the translation of proofs from one Dedukti theory to another and to the exporting of proofs to other proof systems. In particular the Matita arithmetic library has been translated to a much weaker theory: constructive simple type theory, allowing to export it to Coq, Lean, PVS, HOL Light, and Isabelle/HOL. In the same way, the first book of Euclids elements, formalized in Coq has been exported to these systems as well. This led us to develop an online proof repository Nubo and an on-line encyclopedia Logipedia, allowing to share and browse this library.

We also focus on the development of new theories in Dedukti.

Finally, we develop an interactive theorem prover Lambdapi based on the same formalism as Dedukti. This interactive theorem prover is also used as a tool in the process of translating proofs from PVS and from automated theorem provers.

3.1 Logical Frameworks

A thesis, which is at the root of our research effort, is that logical systems should be expressed as theories in a logical framework. As a consequence, proof-checking systems should not be focused on one theory, such as Simple type theory, Martin-Löf's type theory, or the Calculus of constructions, but should be theory independent. On the more theoretical side, the proof search algorithms, or the algorithmic interpretation of proofs should not depend on the theory in which proofs are expressed, but this theory should just be a parameter. This is for instance expressed in the title of our invited talk at ICALP 2012: A theory independent Curry-De Bruijn-Howard correspondence36.

Various limits of Predicate logic have led to the development of various families of logical frameworks: $\lambda$-prolog and Isabelle have allowed terms containing free variables, the Edinburgh logical framework has allowed proofs to be expressed as $\lambda$-terms, Pure type systems have allowed propositions to be considered as terms, and Deduction modulo theory has allowed theories to be defined not only with axioms, but also with computation rules.

The $\lambda \Pi$-calculus modulo theory, that is implemented in the system Dedukti and that is a synthesis of the Edinburgh logical framework and of Deduction modulo theory, subsumes them all.

3.2 Interoperability and proof encyclopediae

Using a single prover to check proofs coming from different systems naturally leads to investigate how these proofs can be translated from one theory to another and used in a system different from the system in which they have been developed. This issue is of prime importance because developments in proof systems are getting bigger and, unlike other communities in computer science, the proof checking community has given little effort in the direction of standardization and interoperability.

For each proof, independently of the system in which it has been developed, we should be able to identify the systems in which it can be expressed. For instance, we have shown that many proofs developed in the Matita prover did not use the full strength of the logic of Matita and could be exported, for instance, to the systems of the HOL family, that are based on a weaker logic.

Rather than importing proofs from one system, transforming them, and exporting them to another system, we can use the same tools to develop a system-independent online repository of proofs Nubo and even a system-independent proof encyclopedia Logipedia. In such a repository, each proof is labeled with the theories in which it can be expressed and so with the systems in which it can be used.

3.3 Interactive theorem proving

We also want to investigate how the $\lambda \Pi$-calculus modulo theory can be used as the basis of an interactive theorem prover. This leads to two new scientific questions: first, how much can a tactic system be theory independent, and then how does rewriting extends the possibility to write tactics.

This has led to the development of Lambdapi, which is an interactive theorem prover for the $\lambda \Pi$-calculus modulo theory. Several tactics have been developed for this system, which are intended to help a human user to write proofs in our system instead of writing proof terms by hand.

3.4 Proof automation

Interoperability between interactive and automatic theorem provers can be fruitful to both systems: results coming from automatic solvers can be checked by a third-party software with an identified kernel, and interactive provers can benefit from more automation. We are pushing towards this last application by extending the SMTCoq plugin for the Coq proof assistant with new logical transformations that encode Coq goals into first-order logic, which is the input logic of the class of automatic provers called SMT solvers.

4.1 Interoperability

Our main impact applications, for instance to proofs of programs, or to air traffic control, are through our cooperation with other teams.

We view our work on interoperability and on the design of a formal proof encyclopedia as a service to the formal proof community.

5.1 Awards

Frédéric Blanqui's European COST project EuroProofNet has been accepted. EuroProofNet is the European research network on digital proofs. It aims at boosting the interoperability and usability of proof systems. It started on November 2021 and already gathers more than 220 researchers from 30 different countries. EuroProofNet organizes meetings and schools, and provides grants to its members for short-term scientific missions in another lab or country.

Frédéric Blanqui and Gabriel Hondet published a new release of the proof assistant Lambdapi. Lambdapi has been used in various works and, in particular, in Quentin Garchery's PhD 38.

Yacine El Haddad defended his PhD thesis on the integration of automated theorem provers in proof assistants 23.

Gilles Dowek and Alejandro Díaz-Caro have received the Best paper award (shared with another paper) at the 18th International Colloquium on Theoretical Aspects of Computing.

Renaud Vilmart received an accessit to the 2020 Gilles Kahn Ph.D. thesis award.

Yoan Géran has received the Best student paper award at the 46th International Symposium on Mathematical Foundations of Computer Science.

5.2 New software

6.1 Development of Lambdapi

Participants: Frédéric Blanqui, Luc Chabassier, Loris Cros, Gabriel Hondet, Thomas Traversié.

Frédéric Blanqui and Gabriel Hondet published a new release of Lambdapi. Lambdapi is a proof assistant for the λΠ-calculus modulo rewriting. It extends Dedukti with meta-variables, implicit arguments, etc. and an interactive proof mode for solving typing and unification goals using tactics. Typing goals corresponding to first-order formulas can be discharged by calling external automated theorem provers via the Why3 library. Lambdapi can read and output Dedukti files and can thus be used as an intermediate higher-level language for translating proofs from one system to Dedukti.

Many improvements have been made on Lambdapi in 2021: parser generator changed to Menhir; generation of induction principles extended to parametrized strictly-positive types; addition of the tactics induction, admit and generalize; addition of associative and commutative symbols; addition of structured proof scripts (Aurélien Castre's internship), improvement of the Emacs and VSCode interface (Ashish Kumar Barnawal).

Lambdapi has been used in 2021 by:

• Luc Chabassier in his master internship to formalize a translation of extensional type theory in Martin-Löf's type theory extended with functional extensionality and uniqueness of identity proofs (Streicher's axiom K).
• Thomas Traversié in his internship to formalize set theory.
• Quentin Garchery in his PhD work for verifying Why3 transformation certificates 38. He also developped a Lambdapi library on binary integers.

Loris Cros, in his internship supervised by Bruno Barras, has continued developing algorithms to check criterions related to confluence of rewrite systems in Dedukti. He also started the implemtation of a completion algorithm in order to deal with rewriting modulo associativity and commutativity (AC).

6.2 Theory of λΠ-calculus modulo rewriting and other logical formalisms

Participants: Frédéric Blanqui, Gilles Dowek, Jean-Pierre Jouannaud.

Gilles Dowek has investigated a alternative presentation of Pure Type Systems, where the notion of well-formed context has been dropped. This work has been published in the proceedings of Logical Frameworks and Meta-Languages 31.

Frédéric Blanqui has investigated and implemented in Lambdapi how to encode type universes without using matching modulo associativity and commutativity, which is complex to implement. It is based on a technique introduced in 34.

Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu have investigated confluence criterions for non-terminating Higher-Order Rewrite Theories.

6.3 New theories in the λΠ-calculus modulo rewriting

Participants: Bruno Barras, Frédéric Blanqui, Valentin Blot, Luc Chabassier, Gilles Dowek, Thiago Felicissimo, Yoan Géran, Émilie Grienenberger, Olivier Hermant, Gabriel Hondet, Amélie Ledein, Yann Leray, Thomas Traversié.

Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and Francois Thiré have studied a theory in Dedukti, called U, that enables to express proofs in various theories (constructive and non constructive predicate logic, constructive and non constructive simple type theory, with and without polymorphism, with and without predicate subtyping, the Calculus of constructions, etc.) and shown that each of these theories corresponds to a selection of axioms in the theory U. This paper has been published in the proceedings of Formal Structures for Computation and Deduction 14.

During his Master internship, Luc Chabassier implemented in lambdapi a translation from the Extensional Type Theory (ETT) to Intensional Type Theory (ITT), inspired from the paper "Eliminating Reflection From Type Theory" (Winterhalter, Sozeau et Tabareau)  42. In contrast to what the authors did, his translation his well-typed by construction, rather than building an untyped term that has to be proved correct after the fact.

During his Master internship, Thiago Felicissimo worked on the translations from the proof assistant Agda to Dedukti and Lambdapi. In particular, he showed how to translate copattern matching coinduction 32, and implemented this in the tool Agda2Dedukti.

Gabriel Hondet and Frédéric Blanqui showed how to encode in the λΠ-calculus modulo rewriting, predicate subtyping and proof irrelevance, two important features of the PVS proof assistant. They proved that this encoding is correct and that encoded proofs can be mechanically checked by Dedukti, a type checker for the λΠ-calculus modulo theory using rewriting 39.

Luc Chabassier has started a Phd, supervised by Bruno Barras and Gilles Dowek, which goal is to study new approaches to formalize Category Theory in proof assistants, potentially exploiting the rewriting features of Dedukti.

Yoan Géran has started a Phd, supervised by Olivier Hermant and Gilles Dowek, on reverse mathematics in Dedukti. His objective is to refine the translation framework from Coq to Dedukti with a focus on universes, to develop the corresponding tool, Vodk, along with reverse mathematics techniques to analyze and minimize the Dedukti proofs.

Thomas Traversié, during his internship supervised by Valentin Blot and Gilles Dowek, implemented set theory in Lambdapi. In particular, he encoded sets by a structure of pointed graphs, following the lines given in the paper "Cut elimination for Zermelo set theory" (Dowek and Miquel)  37.

Yann Leray improved and developed the translations from the proof assistant Isabelle to Lambdapi and Dedukti 30.

During her thesis, which started in October 2020, Amélie Ledein is interested in the verification of formal semantics proofs (such as the proof that a language is deterministic or the so-called subject reduction property) of programming languages as well as the reuse of these proofs in another proof assistant. A first result obtained concerns the translation of K, a framework for defining formal semantics of programming languages from which different tools are automatically derived, into Dedukti. The implementation of this translation, named KaMeLo, is available here. This work was presented during an LVP research day in 2021, and will be published at the JFLA national conference in June 2022.

6.4 Translation from one theory to another

Participants: Frédéric Blanqui, Guillaume Burel, Yacine El Haddad, Gabriel Hondet.

Gabriel Hondet investigated how to translate theories with implicit subtyping into Lambdapi without translating the subtyping derivations. The framework has been modified to be able to synthesise back the subtyping derivations using a generic coercion insertion algorithm. The mechanism has been implemented in the tool Personoj and tested on the translation of the standard library of PVS.

Yacine El Haddad, Guillaume Burel and Frédéric Blanqui showed the correctness of a de-skolemization transformation consisting in building a proof in a deep encoding of natural deduction in the λΠ-calculus modulo rewriting of a first-order formula from a proof of its skolemization. This transformation has been implemented in the tool SKonverto.

Yacine El Haddad defended his PhD thesis on the integration of automated theorem provers in proof assistants 23. His contributions are:

• Calling external provers. Since the provers do not use the same logic and system as the proof assistant, we elaborated a translation between Lambdapi’s logic which is the λΠ-calculus Modulo Theory and the provers’ logic which is first-order logic. This translation is implemented inside Lambdapi as part of its tactic language. Moreover, we showed that this translation is correct, i.e., if there is a proof of the translation of a formula in first-order logic, then there is a proof of that formula in the λΠ-calculus Modulo Theory.
• Reconstructing proofs. Proof assistants do not always support the output of external provers. However, for some proof assistants, there is a prover that outputs a format supported by that proof assistant. This is the case of Lambdapi with ZenonModulo and ArchSAT, and Coq with Zenon. We designed an architecture to reconstruct proofs generated by provers into Lambdapi by detecting which information is missing and asking a prover supported by Lambdapi to generate that missing information. The proposed solution does not depend on a specific prover and can reconstruct a considerable amount of proofs. The output format of the provers chosen is TSTP since it is the standard format used to test automated theorem provers. This solution is implemented as an independent tool named Ekstrakto.
• Transforming Skolemized proofs. Provers can use many techniques to prove a formula, and one of these techniques is Skolemization. This transformation step transforms the original formula into an equi-satisfiable but not syntactically equivalent formula. We implemented an algorithm that transforms the proof of the new formula into a proof of the original one. The presented algorithm is proved correct and could be used separately if the proof fits a particular specification. This algorithm is implemented as a tool named SKonverto, which could be used with Ekstrakto to build proofs in Lambdapi.

Yoan Géran, during his internship, has analyzed the GeoCoq proof library, that contain the proofs of Euclid's Elements, book I. He has shown that it can be shrinked from the Calculus of Constructions with universes to fit in a logic as weak as predicate logic. Through the tools developed at Deducteam, this allowed GeoCoq to be exported to 7 systems : HOL Light, Lean, Matita, OpenTheory (hence Isabelle/HOL and HOL4), and PVS.

6.5 Automation for the Coq proof assistant

Participants: Valentin Blot, Louise Dubois de Prisque, Pierre Vial.

In order to automatize the Coq proof assistant, tactics which send a first-order goal to SMT solvers are available in the SMTCoq plugin.

Valentin Blot, Louise Dubois de Prisque and Pierre Vial, with the external collaboration of Chantal Keller, developed a new Coq automatic tactic15 which generates and proves first-order statements about Coq terms (datatypes and functions). This enriches the semantics of information transmitted to SMTCoq and increases automation in the Coq proof assistant.

This tactic snipe is modular and combines independent transformations, which allows incremental development.

6.6 Theory of inductive definitions

Participants: Catherine Dubois, Amélie Ledein.

Catherine Dubois, Amélie Ledein and Mathieu Montin (Loria) have developed the LIBNDT library, implemented both in Agda and Coq, concerning a class of nested inductive types. This library proposes a generic type LNDT (linked nested datatype) of which some common data types (List, Maybe, Nest and even Bush - in Agda only for the latter) can be constructed as various instances. A paper has been accepted for publication in the international workshop MSFP 2022 (Mathematically Structured Functional Programming).

6.7 Quantum Computing

Participants: Pablo Arnault, Gilles Dowek, Renaud Vilmart.

Gilles Dowek and Alejandro Díaz-Caro have investigated an extension of propositional logic with a new connective, called sup, that has the introduction rules of the conjunction and the elimination rules of the disjunction and shown that this connective enables to model non-deterministic and non-reversible processes such as quantum measurement. This work 25 has been published in the proceedings of the 18th International Colloquium on Theoretical Aspects of Computing, where it has received the Best paper award (shared with another paper).

Renaud Vilmart, together with collaborators Benoît Valiron and Kostia Chardonnet have laid the foundations for a geometry of interaction-style of semantics for graphical language ZX-Calculus, devoted to quantum computing. This paper has been published in the proceedings of MFCS 2021 17, and also in the proceedings of TLLA 20121 16.

Renaud Vilmart has investigated the links between graphical language ZH-Calculus and Quantum Multiple-valued Decision Diagrams (QMDDs) used in verification of quantum processes. This paper has been published in the proceedings of MFCS 2021 19.

Renaud Vilmart has published a paper at FoSSaCS 2021 41. This paper does not appear in the team's publications, as it was submitted before the author joined Deducteam.

Pablo Arnault has introduced a discrete-time quantum walk (DQW) defined on a polar grid, a primer, and are hence able to define an angular momentum for this DQW, which is conserved at the discrete level, i.e., on the spacetime lattice. Ha has shown that in the continuum limit the standard relativistic Landau levels of the Dirac equation are recovered in the case the Hamiltonian has been codiagonalized with, not the linear momentum, but the angular one. Those results have been published in  13.

Pablo Arnault has shown that one can discretize the Dirac equation under the form of a DQW without specifying a particular representation of the Clifford algebra. A new Clifford algebra has been defined from the operators defining the DQW, by requiring that the square of the DQW delivers what we define as a valid discretization of the Dirac equation (this parallels exactly, at the discrete level, Dirac’s original procedure in the continuum). We then show that the DQW contains, natively, a Wilson term that enables to avoid fermion doubling, and this without breaking unitarity, while discrete-time versions of standard lattice gauge theory are usually formulated in a Lagrangian way so that unitarity is not in-built, has to be proven, and is actually frequently broken. Those results appear in  24.

7.1 Bilateral contracts with industry

Participants: Valentin Blot.

Valentin Blot and Chantal Keller have funding for a 4-year project (2021–2025) involving a PhD student, a research engineer (2 years) and a post-doctoral researcher (2 years). This funding is part of the Inria - Nomadic labs partnership for Tezos blockchain.

8.1 International initiatives

8.2 International research visitors

8.3 European initiatives

8.4 National initiatives

Participants: Gilles Dowek, Catherine Dubois.

The ANR project (2022-2025) ICSPA (Interoperable and Confident Set-based Proof Assistants) has been accepted in the context of the AAPG 2021 call. It is coordinated by Catherine Dubois and has the following academic partners Samovar – Inria Grand Est – Inria Paris-Saclay – LIRMM – IRIT with the industrial partner Clearsy. The project starts on January 1st 2022. This project aims at reinforcing the confidence in proofs carried out mechanically for the set-based specification formalisms B, Event-B, and TLA+ that are used in industry.This will be done by verifying these proofs formally and independently with the proof verifier Dedukti. The project also aims at designing and implementing an exchange framework, through which those three systems can share their proofs and theories, making them effectively interoperable.

The ANR PROGRAMme is an ANR for junior researcher Liesbeth Demol (CNRS, UMR 8163 STL, University Lille 3) to which G. Dowek participates. The subject is: “What is a program? Historical and Philosophical perspectives”. This project aims at developing the first coherent analysis and pluralistic understanding of “program” and its implications to theory and practice.

9.1 Promoting scientific activities

9.2 Teaching - Supervision - Juries

9.3 Popularization

10.1 Major publications

• 1 inproceedingsA.Ali Assaf, G.Guillaume Burel, R.Raphaël Cauderlier, D.David Delahaye, G.Gilles Dowek, C.Catherine Dubois, F.Frédéric Gilbert, P.Pierre Halmagrand, O.Olivier Hermant and R.Ronan Saillard. Expressing theories in the $$$$-calculus modulo theory and in the Dedukti system.22nd International Conference on Types for Proofs and Programs, TYPES 2016Novi SAd, SerbiaMay 2016
  HAL
• 2 articleB.Bruno Barras, T.Thierry Coquand and S.Simon Huber. A generalization of the Takeuti-Gandy interpretation.Mathematical Structures in Computer Science2552015, 1071--1099URL: https://doi.org/10.1017/S0960129514000504
  DOI
• 3 articleF.Frédéric Blanqui. Definitions by rewriting in the Calculus of Constructions.Mathematical Structures in Computer Science1512005, 37-92
  HALDOI
• 4 articleF.Frédéric Blanqui, J.-P.Jean-Pierre Jouannaud and A.Albert Rubio. The Computability Path Ordering.Logical Methods in Computer ScienceOctober 2015
  HALDOI
• 5 inproceedingsV.Valentin Blot. An interpretation of system F through bar recursion.32nd ACM/IEEE Symposium on Logic in Computer ScienceIEEE2017
• 6 articleG.Guillaume Burel, G.Guillaume Bury, R.Raphaël Cauderlier, D.David Delahaye, P.Pierre Halmagrand and O.Olivier Hermant. First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice.Journal of Automated Reasoning2019
  HALDOI
• 7 inproceedingsD.Denis Cousineau and G.Gilles Dowek. Embedding Pure Type Systems in the $$$$-calculus modulo.Typed lambda calculi and applications4583Lecture Notes in Computer ScienceSpringer-Verlag2007, 102-117
• 8 articleG.Gilles Dowek, T.Thérèse Hardin and C.Claude Kirchner. Theorem proving modulo.Journal of Automated Reasoning312003, 33-73
• 9 articleO.Olivier Hermant. Resolution is Cut-Free.Journal of Automated Reasoning443March 2010, 245-276
• 10 articleM.Mélanie Jacquel, K.Karim Berkani, D.David Delahaye and C.Catherine Dubois. Tableaux Modulo Theories Using Superdeduction.Global Journal of Advanced Software Engineering (GJASE)1December 2014, 1-13
  HALDOI
• 11 articleM.Mélanie Jacquel, K.Karim Berkani, D.David Delahaye and C.Catherine Dubois. Verifying B Proof Rules using Deep Embedding and Automated Theorem Proving.Software and Systems Modeling (SoSyM)June 2013

10.2 Publications of the year

10.3 Cited publications

• 33 unpublishedP.Pablo Arnault. Clifford algebra from quantum automata and unitary Wilson fermions.February 2022, working paper or preprint
  HALback to text
• 34 inproceedingsF.F. Blanqui, T.T. Hardin and P.P. Weis. ://doi.org/10.1007/978-3-540-71316-68On the implementation of construction functions for non-free concrete data types.Proceedings of the 16th European Symposium on Programming\em, Lecture Notes in Computer Science 442115 pages2007
  back to text
• 35 phdthesisM.Mathieu Boespflug. Conception d'un noyau de vérification de preuves pour le $$-calcul modulo.École Polytechnique2011
  back to text
• 36 inproceedingsG.Gilles Dowek. A Theory Independent Curry-de Bruijn-howard Correspondence.Proceedings of the 39th International Colloquium Conference on Automata, Languages, and Programming - Volume Part IIICALP'12Berlin, HeidelbergWarwick, UKSpringer-Verlag2012, 13--15URL: http://dx.doi.org/10.1007/978-3-642-31585-5_2
  DOIback to text
• 37 articleG.G. Dowek and A.A. Miquel. Cut elimination for Zermelo set theory.Manuscript, available from the web pages of the authors2007
  back to text
• 38 inproceedingsQ.Q. Garchery. ://doi.org/10.4204/EPTCS.336.2A Framework for Proof-carrying Logical Transformations.Proceedings of the 7th International Workshop on Proof eXchange for Theorem Proving\em, Electronic Proceedings in Theoretical Computer Science 3362021
  back to textback to text
• 39 inproceedingsG.G. Hondet and F.F. Blanqui. ://doi.org/10.4230/LIPIcs.TYPES.2020.6Encoding of Predicate Subtyping and Proof Irrelevance in the $$-calculus Modulo Theory.Proceedings of the 26th International Conference on Types for Proofs and Programs\em, Leibniz International Proceedings in Informatics 1882021
  back to text
• 40 articleG.Gareth Jay, P.Pablo Arnault and F.Fabrice Debbasch. Dirac quantum walks with conserved angular momentum.Quantum Studies: Mathematics and Foundations84November 2021, 419-430
  HALDOIback to text
• 41 inproceedingsR.Renaud Vilmart. The Structure of Sum-Over-Paths, its Consequences, and Completeness for Clifford.Foundations of Software Science and Computation StructuresChamSpringer International Publishing2021, 531--550
  back to text
• 42 inproceedingsT.Théo Winterhalter, M.Matthieu Sozeau and N.Nicolas Tabareau. Eliminating reflection from type theory.Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019ACM2019, 91--103URL: https://doi.org/10.1145/3293880.3294095
  DOIback to text