Skip to content

Edit affiliation: 13 and two missed typos #2828

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Sep 10, 2025
Merged

Edit affiliation: 13 and two missed typos #2828

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f1a713a
Add missed backtick and an i
shhyou Sep 10, 2025
c2fbe81
Fix affiliation 13 index
shhyou Sep 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions paper/paper.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,8 @@ authors:
orcid: 0000-0003-2673-4400
affiliation: 12
- name: You, Shu-Hung
affiliation: 12
orcid: 0009-0003-0003-3945
affiliation: 13
- name: Mullanix, Reed
orcid: 0000-0002-7970-4961
affiliation: 9
Expand Down Expand Up @@ -159,7 +160,7 @@ On the other hand, `batteries` and `mathlib` [@van2020maintaining] for Lean prov
Philosophically, `agda-stdlib` is more closely aligned with the approach of the MathLib library, and our aim is to provide canonical definitions for mathematical objects and introduce new representations only sparingly.

A second challenge is that `agda-stdlib` has embraced the "intrinsic style" of dependent types, in which correctness-related invariants are part of data structures, rather than separate predicates.
Many definitions in agda-stdlib use this intrinsic style.
Many definitions in `agda-stdlib` use this intrinsic style.
For instance, the final definition of rational numbers is a record type that alongside the numerator and denominator contains a proof showing that the numerator and denominator have no common factors.
The intrinsic style also includes returning proofs rather than, say, booleans from decision procedures.
The standard library for instance uses this approach for its implementation of regular expression matching which along with the match returns a proof justifying it.
Expand Down Expand Up @@ -208,7 +209,7 @@ The authors of this paper are listed approximately in order of contribution to t
# Funding and conflicts of interest

The authors of this paper have no conflicts of interest to declare.
Many of the contributions to the library by the authors of this paper were made over a significant period of time and while at other institutions than their current affliation. Some of the contributions have been made while receiving funding for related projects, and a non-exhaustive list of such funding follows:
Many of the contributions to the library by the authors of this paper were made over a significant period of time and while at other institutions than their current affiliation. Some of the contributions have been made while receiving funding for related projects, and a non-exhaustive list of such funding follows:

- Jason Z. S. Hu made his contributions during his funded Master's and PhD study.

Expand Down