Skip to content

Commit

Permalink
Fix affliations
Browse files Browse the repository at this point in the history
  • Loading branch information
MatthewDaggitt committed Dec 9, 2024
1 parent c4b1d6b commit 91b9a5e
Showing 1 changed file with 29 additions and 30 deletions.
59 changes: 29 additions & 30 deletions paper/paper.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,77 +11,77 @@ authors:
corresponding: true
affiliation: 1
- name: Danielsson, Nils Anders
affliation: 11
affliation: 2
- name: Allais, Guillaume
orcid: 0000-0002-4091-657X
affiliation: 2
affiliation: 3
- name: McKinna, James
orcid: 0000-0001-6745-2560
affiliation: 4
- name: Abel, Andreas
orcid: 0000-0003-0420-4492
affiliation: 11
affiliation: 2
- name: van Doorn, Nathan
orcid: 0009-0009-0598-3663
affiliation: 5
- name: Wood, James
orcid: 0000-0002-8080-3350
affiliation: 13
affiliation: 6
- name: Norell, Ulf
orcid: 0000-0003-2999-0637
affiliation: 11
affiliation: 2
- name: Kidney, Donnacha Oisín
orcid: 0000-0003-4952-7359
affiliation: 9
affiliation: 7
- name: Meshveliani, Sergei
orcid: 0000-0002-4224-6178
affiliation: 10
affiliation: 8
- name: Carette, Jacques
orcid: 0000-0001-8993-9804
affiliation: 3
affiliation: 9
- name: Rice, Alex
orcid: 0000-0002-2698-5122
affiliation: 7
affiliation: 10
- name: Hu, Jason Z. S.
orcid: 0000-0001-6710-6262
affiliation: 6
affiliation: 11
- name: Xia, Li-yiao
orcid: 0000-0003-2673-4400
affiliation: 8
affiliation: 12
- name: You, Shu-Hung
affliation: 12
affliation: 13
- name: Mullanix, Reed
orcid: 0000-0002-7970-4961
affiliation: 3
affiliation: 9
- name: Kokke, Wen
orcid: 0000-0002-1662-0381
affiliation: 7
affiliation: 10
affiliations:
- name: University of Western Australia, Australia
index: 1
- name: University of Strathclyde, United Kingdom
- name: University of Gothenburg and Chalmers University of Technology, Sweden
index: 2
- name: McMaster University, Canada
- name: University of Strathclyde, United Kingdom
index: 3
- name: Heriot-Watt University, United Kingdom
index: 4
- name: Independent Software Developer
index: 5
- name: Amazon, USA
- name: Huawei Technologies Research & Development, United Kingdom
index: 6
- name: University of Edinburgh, United Kingdom
- name: Imperial College London, United Kingdom
index: 7
- name: INRIA, France
- name: Russian Academy of Sciences, Russia
index: 8
- name: Imperial College London, United Kingdom
- name: McMaster University, Canada
index: 9
- name: Russian Academy of Sciences, Russia
- name: University of Edinburgh, United Kingdom
index: 10
- name: University of Gothenburg and Chalmers University of Technology, Sweden
- name: Amazon, USA
index: 11
- name : Northwestern University, USA
- name: INRIA, France
index: 12
- name : Huawei Technologies Research & Development, United Kingdom
- name : Northwestern University, USA
index: 13
date: 24 September 2024
bibliography: paper.bib
Expand All @@ -93,10 +93,9 @@ Agda [@agda2024manual] is a dependently-typed functional
language that serves both as a traditional programming language
and as an interactive theorem prover (ITP).
In other words, its type system is expressive enough to formulate
complex formal requirements, and its compiler lets users interactively
build programs guaranteed to meet these specifications.
complex formal requirements as types, and its compiler allows users to interactively build terms and check that they satisfy these requirements.
Through the Curry-Howard lens [@DBLP:journals/cacm/Wadler15],
these types and programs can be seen respectively as theorem
these types and terms can be seen respectively as theorem
statements and proofs.

This paper presents the Agda standard library [@agda-stdlib-v2.0], hereafter referred to as `agda-stdlib`, which provides definitions intended to be helpful for users to develop Agda programs and proofs.
Expand All @@ -115,7 +114,7 @@ This lack of basic data types increases the need for a standard library when com

Second, Agda users often seek to prove that programs constructed using data types in the standard library are "correct."
Constructing the proof that a function obeys a specification (e.g. that a sorting function outputs a permutation of the original list in non-decreasing order) typically requires far more effort, both in terms of lines of code and in developer time, than writing the original operation.
By frequently providing proofs of correctness for the operations it defines, the standard library saves users significant time during proof development.
By providing proofs of correctness for the operations it defines, the standard library saves users significant time during proof development.

# Impact

Expand All @@ -137,7 +136,7 @@ In the list below we present a selection of such projects:
The library has also been used as a test bed for the design of co-inductive data types in Agda itself, as evidenced by the three different notions of co-inductive data present in the library.

On occasion, the development of `agda-stdlib` has also had a synergistic relationship with that of Agda itself, prompting the implementation of several new language features, which we now discuss.
Firstly, Agda is a research compiler supporting a wide range of not necessarily inter-compatible language extensions via command line options.
Firstly, Agda is a research compiler supporting a wide range of possibly incompatible language extensions via command line options.
Examples include `--cubical` (changing the underlying type theory to cubical type theory [@DBLP:journals/jfp/VezzosiMA21]),
`--with-K` (adding support for Streicher's axiom K [@streicher1993investigations], a reasoning principle incompatible with the `--cubical`-enabled type theory),
or `--safe` (an ITP-oriented option enforcing that nothing is postulated and disabling parts of the FFI mechanism).
Expand All @@ -147,7 +146,7 @@ To enable this, in 2019 Agda's language options were categorised as "infective",
Once used in a module, an "infective" option will impact all the import*ing* modules; these are typically for theory-changing options like `--cubical` or `--with-K`.
On the contrary, "coinfective" options affect the import*ed* modules; these are typically for options adding extra safety checks like `--safe`.
This categorisation enables libraries to integrate safe Agda code with code that uses unsafe operating system calls, while maintaining the safety guarantees of the former.
Secondly, the development of `agda-stdlib` motivated adding the ability to attach custom messages to definitions, which are then displayed by the compiler when the definitions are used.
Another feature motivated by the development of `agda-stdlib` is the ability to attach custom messages to definitions, which are then displayed by the compiler when the definitions are used.
This enabled the implementation of deprecation warnings, which makes it easier for end-users to evolve their code alongside new versions of `agda-stdlib`.

# Design
Expand Down

0 comments on commit 91b9a5e

Please sign in to comment.