activity
20202025
most citedFormalized Class Group Computations and Integral Points on Mordell Elliptic Curves

6 citations · 10 across the 5 of their papers we have counts for

collaborators
Showing cs.LOShow all

5 papers · 1 filter

cs.LO2024

Certifying rings of integers in number fields

Anne Baanen, Alain Chavarri Villarello, Sander R. Dahmen

Number fields and their rings of integers, which generalize the rational numbers and the integers, are foundational objects in number theory. There are several computer algebra sys…

cs.LO2022★ 6 cited

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

Anne Baanen, Alex J. Best, Nirvana Coppola +1

Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form , where is a (gi…

cs.LO2022★ 3 cited

Use and abuse of instance parameters in the Lean mathematical library

Anne Baanen

The Lean mathematical library mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean's mechanism of instance parameters. Rela…

cs.LO2021

A formalization of Dedekind domains and class groups of global fields

Anne Baanen, Sander R. Dahmen, Ashvni Narayanan +1

Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental pro…

cs.LO2020★ 1 cited

Combining predicate transformer semantics for effects: a case study in parsing regular languages

Anne Baanen, Wouter Swierstra

This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our p…