The FacetedDBLP logo    Search for: in:

Disable automatic phrases ?     Syntactic query expansion: ?

Publications at "CPP"( http://dblp.L3S.de/Venues/CPP )

URL (DBLP): http://dblp.uni-trier.de/db/conf/cpp

Publication years (Num. hits)
2011 (29) 2012 (23) 2013 (20) 2015 (21) 2016 (21) 2017 (22) 2018 (25) 2019 (22) 2020 (30) 2021 (27) 2022 (28) 2023 (28) 2024 (22)
Publication types (Num. hits)
inproceedings(305) proceedings(13)
Venues (Conferences, Journals, ...)
CPP(318)
GrowBag graphs for keyword ? (Num. hits/coverage)

Group by:
No Growbag Graphs found.

Results
Found 318 publication records. Showing 318 according to the selection in the facets
Hits ? Authors Title Venue Year Link Author keywords
1Azalea Raad Under-Approximation for Scalable Bug Detection (Keynote). Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Duc-Than Nguyen, Lennart Beringer, William Mansky, Shengyi Wang Compositional Verification of Concurrent C Programs with Search Structure Templates. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1David Monniaux Memory Simulations, Security and Optimization in a Verified Compiler. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Ike Mulder, Robbert Krebbers Unification for Subformula Linking under Quantifiers. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Nao Hirokawa, Dohan Kim 0001, Kiraku Shintani, René Thiemann Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1María Inés de Frutos-Fernández, Filippo Alberto Edoardo Nuccio Mortarino Majno di Capriglio A Formalization of Complete Discrete Valuation Rings and Local Fields. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Chelsea Edmonds, Lawrence C. Paulson Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur 0001, Ilya Sergey Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Joseph Eremondi Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Niels van der Weide, Nima Rasekh, Benedikt Ahrens, Paige Randall North Univalent Double Categories. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Nikolai Kudasov, Emily Riehl, Jonathan Weinberger Formalizing the ∞-Categorical Yoneda Lemma. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Andrew W. Appel, Ariel Kellison VCFloat2: Floating-Point Error Analysis in Coq. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy (eds.) Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024 Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, Loïc Pujet Martin-Löf à la Coq. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Ana de Almeida Borges, Mireia González Bedmar, Juan José Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost J. Joosten UTC Time, Formally Verified. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Ian Shillito, Dominik Kirst A Mechanised and Constructive Reverse Analysis of Soundness and Completeness of Bi-intuitionistic Logic. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Siddhartha Gadgil, Anand Rao Tadipatri Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Lauren White, Laura Titolo, J. Tanner Slagel, César A. Muñoz A Temporal Differential Dynamic Logic Formal Embedding. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Benedikt Ahrens, Ralph Matthes, Niels van der Weide, Kobe Wullaert Displayed Monoidal Categories for the Semantics of Linear Logic. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Ekaterina Zhuchko, Margus Veanes, Gabriel Ebner Lean Formalization of Extended Regular Expression Matching with Lookarounds. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Clément Chavanon, Frédéric Besson, Tristan Ninet PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams. Search on Bibsonomy CPP The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
1Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, Nate Foster P4Cub: A Little Language for Big Routers. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Reynald Affeldt, Cyril Cohen, Ayumu Saito Semantics of Probabilistic Programs using s-Finite Kernels in Coq. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Hugo Férée, Sam van Gool Formalizing and Computing Propositional Quantifiers. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Anthony Bordg, Adrián Doña Mateo Encoding Dependently-Typed Constructions into Simple Type Theory. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Kexing Ying, Rémy Degenne A Formalization of Doob's Martingale Convergence Theorems in mathlib. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi 0001 Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Jannis Limperg, Asta Halkjær From Aesop: White-Box Best-First Proof Search for Lean. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Arvind Arasu, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Aymeric Fromherz, Kesha Hietala, Bryan Parno, Ravi Ramamurthy FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Yannick Forster 0002, Felix Jahn, Gert Smolka A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Cezary Kaliszyk Improved Assistance for Interactive Proof (Keynote). Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Katherine Kosaian, Yong Kiam Tan, André Platzer A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Sandrine Blazy CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Thomas Lamiaux, Axel Ljungström, Anders Mörtberg Computing Cohomology Rings in Cubical Agda. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Bhavik Mehta Formalising Sharkovsky's Theorem (Proof Pearl). Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Christina Kohl, Aart Middeldorp A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic (eds.) Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023 Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Floris van Doorn, Patrick Massot, Oliver Nash Formalising the h-Principle and Sphere Eversion. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Anne Baanen, Alex J. Best, Nirvana Coppola, Sander R. Dahmen Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Valentin Blot, Denis Cousineau 0002, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, Pierre Vial Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Michael Färber 0002 Terms for Efficient Proof Checking and Parsing. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Brae J. Webb, Ian J. Hayes, Mark Utting Verifying Term Graph Optimizations using Isabelle/HOL. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Joshua Clune A Formalized Reduction of Keller's Conjecture. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub A Formal Disproof of Hirsch Conjecture. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Yann Herklotz, Delphine Demange, Sandrine Blazy Mechanised Semantics for Gated Static Single Assignment. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Eske Hoy Nielsen, Danil Annenkov, Bas Spitters Formalising Decentralised Exchanges in Coq. Search on Bibsonomy CPP The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
1Louis Cheung, Liam O'Connor, Christine Rizkallah Overcoming restraint: composing verification of foreign functions with cogent. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman A verified algebraic representation of cairo program execution. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1César Muñoz Structural embeddings revisited (invited talk). Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1William Schultz, Ian Dardik, Stavros Tripakis Formal verification of a distributed dynamic reconfiguration protocol. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle A compositional proof framework for FRETish requirements. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Patricia Johann, Enrico Ghiorzi (Deep) induction rules for GADTs. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Dan Frumin Semantic cut elimination for the logic of bunched implications, formalized in Coq. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Mark Koch, Dominik Kirst Undecidability, incompleteness, and completeness of second-order logic in Coq. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Pablo Donato, Pierre-Yves Strub, Benjamin Werner A drag-and-drop proof tactic. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Cyril Six, Léo Gourdin, Sylvain Boulmé, David Monniaux, Justus Fasse, Nicolas Nardino Formally verified superblock scheduling. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Jonathan Prieto-Cubides On homotopy of walks and spherical maps in homotopy type theory. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt Forward build systems, formally. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Oliver Nash Formalising lie algebras. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Denis Firsov, Dominique Unruh Reflection, rewinding, and coin-toss in EasyCrypt. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1June Andronick The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk). Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Benedikt Ahrens, Ralph Matthes, Anders Mörtberg Implementing a category-theoretic framework for typed abstract syntax. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Guillaume Ambal, Sergueï Lenglet, Alan Schmitt Certified abstract machines for skeletal semantics. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Mihails Milehins An extension of the framework types-to-sets for Isabelle/HOL. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Derek Egolf, Sam Lasser, Kathleen Fisher Verbatim++: verified, optimized, and semantically rich lexing with derivatives. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Andrei Popescu 0001, Steve Zdancewic (eds.) CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022 Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Andrew W. Appel Coq's vibrant ecosystem for verification engineering (invited talk). Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Hing-Lun Chan Windmills of the minds: an algorithm for fermat's two squares theorem. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli Applying formal verification to microkernel IPC at meta. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Michael Färber 0002 Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Simon Friis Vindum, Dan Frumin, Lars Birkedal Mechanized verification of a fine-grained concurrent queue from meta's folly library. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Ariel Kellison A machine-checked direct proof of the Steiner-lehmus theorem. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Shuanglong Kan, Anthony Widjaja Lin, Philipp Rümmer, Micha Schrader CertiStr: a certified string solver. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Alexandre Moine 0001, Arthur Charguéraud, François Pottier Specification and verification of a transient stack. Search on Bibsonomy CPP The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
1Elliot Catt, Michael Norrish On the formalisation of Kolmogorov complexity. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1C. H. R. Chhak, Andrew Tolmach, Sean Noble Anderson Towards formally verified compilation of tag-based policy enforcement. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Véronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rébecca Zucchini A Coq formalization of data provenance. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Tobias Nipkow Teaching algorithms and data structures with a proof assistant (invited talk). Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Martin Desharnais, Stefan Brunthaler 0001 Towards efficient and verified virtual machines for dynamic languages. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. Formal verification of authenticated, append-only skip lists in Agda. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Dominik Kirst, Felix Rech The generalised continuum hypothesis implies the axiom of choice in Coq. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Jannis Limperg A novice-friendly induction tactic for lean. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Johan Commelin, Robert Y. Lewis Formalizing the ring of Witt vectors. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Andreas Lööw Lutsig: a verified Verilog compiler for verified circuit development. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Max W. Haslbeck, René Thiemann An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Sophie Tourret, Jasmin Blanchette A modular Isabelle framework for verifying saturation provers. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Jason Z. S. Hu, Jacques Carette Formalizing category theory in Agda. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Simon Friis Vindum, Lars Birkedal Contextual refinement of the Michael-Scott queue (proof pearl). Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1J. Tanner Slagel, Lauren White, Aaron Dutle Formal verification of semi-algebraic sets and real analytic functions. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Olivier Laurent 0001 An anti-locally-nameless approach to formalizing quantifiers. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee 0001, Jean-Baptiste Tristan A formal proof of PAC learnability for decision stumps. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Koundinya Vajjha, Avraham Shinnar, Barry M. Trager, Vasily Pestun, Nathan Fulton CertRL: formalizing convergence proofs for value and policy iteration in Coq. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters Extracting smart contracts tested and verified in Coq. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Catalin Hritcu, Andrei Popescu 0001 (eds.) CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021 Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Peter Sewell Underpinning the foundations: sail-based semantics, testing, and reasoning for production and CHERI-enabled architectures (invited talk). Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
1Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, Rupak Majumdar Lassie: HOL4 tactics by example. Search on Bibsonomy CPP The full citation details ... 2021 DBLP  DOI  BibTeX  RDF
Displaying result #1 - #100 of 318 (100 per page; Change: )
Pages: [1][2][3][4][>>]
Valid XHTML 1.1! Valid CSS! [Valid RSS]
Maintained by L3S.
Previously maintained by Jörg Diederich.
Based upon DBLP by Michael Ley.
open data data released under the ODC-BY 1.0 license