Commutative algebras of series in Agda

Clemente, Lorenzo

doi:10.4230/artifacts.26956

Artifact

Commutative algebras of series in Agda Software

Author Lorenzo Clemente

Part of: Collection: Supplementary Materials
License: GNU General Public License v3.0 or later
Publication Date: 2026-07-09

Document Identifiers

DOI: 10.4230/artifacts.26956
URN: urn:nbn:de:0030-drops-269560

Author Details

Lorenzo Clemente

Department of Mathematics, Mechanics, and Computer Science, University of Warsaw, Poland

Content

Software (Agda formalisation source code): https://github.com/lclem/lics2026-agda/
archived version

Version/Status

Content created at: 2026-01-15

Cite As Get BibTex

Lorenzo Clemente. Commutative algebras of series in Agda (Software, Agda formalisation source code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/artifacts.26956

Description

This repository contains the literate Agda formalisation for the paper "Commutative algebras of series" by Lorenzo Clemente (LICS’26). Background, motivation, and examples are given in the paper, which contains clickable links to the relevant parts of this website. We develop a fragment of the theory of formal series in noncommuting variables and their algebraic properties. Our approach is coinductive, using Agda’s sized types and guardedness features. This website is meant to be accessible without referring to the paper. In particular, it can be used as a tutorial on the formalisation of power series in Agda. Clicking on a keyword will take you to its definition.

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata

0

Downloads

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail