Skip to content

Commit 2e56430

Browse files
committed
fix: refs
1 parent d45ba4a commit 2e56430

File tree

2 files changed

+16
-15
lines changed

2 files changed

+16
-15
lines changed

docs/main.typ

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@
2121
#set page(numbering : "1")
2222

2323
#counter(page).update(1)
24-
#set cite(style: "institute-of-physics-numeric")
24+
#set cite(style: "the-institution-of-engineering-and-technology")
2525

2626
#include "introduction.typ"
2727

docs/refs.bib

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,11 @@ @article{iris
99
} <div></div>
1010
1111
@article{sozeau:inria-00628904,
12-
title = {{A New Look at Generalized Rewriting in Type Theory}},
12+
title = {A New Look at Generalized Rewriting in Type Theory},
1313
author = {Sozeau, Matthieu},
1414
url = {https://inria.hal.science/inria-00628904},
15-
journal = {{Journal of Formalized Reasoning}},
16-
publisher = {{ASDD-AlmaDL}},
15+
journal = {Journal of Formalized Reasoning},
16+
publisher = {ASDD-AlmaDL},
1717
volume = {2},
1818
number = {1},
1919
pages = {41-62},
@@ -27,14 +27,14 @@ @manual{coqmorphism
2727
title = {Library Coq.Classes.Morphisms},
2828
author = {Matthieu Sozeau},
2929
organization = {LRI, CNRS UMR 8623 - University Paris Sud},
30-
address = {https://rocq-prover.org/doc/v8.20/stdlib/Coq.Classes.Morphisms.html},
30+
url = {https://rocq-prover.org/doc/v8.20/stdlib/Coq.Classes.Morphisms.html},
3131
edition = {20},
3232
month = {September},
3333
year = {2024}
3434
}
3535

3636
@misc{casteran:hal-00702455,
37-
title = {{A gentle introduction to type classes and relations in Coq}},
37+
title = {A gentle introduction to type classes and relations in Coq},
3838
author = {Cast{\'e}ran, Pierre and Sozeau, Matthieu},
3939
url = {https://hal.science/hal-00702455},
4040
note = {This document presents the main features of type classes and user-defined relations in the Coq proof assistant. Available at http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf},
@@ -46,7 +46,7 @@ @misc{casteran:hal-00702455
4646

4747
@misc{selsam2020tabledtypeclassresolution,
4848
title = {Tabled Typeclass Resolution},
49-
author = {Daniel Selsam and Sebastian Ullrich and Leonardo de Moura},
49+
author = {Selsam, Daniel and Ullrich, Sebastian and de Moura, Leonardo},
5050
year = {2020},
5151
eprint = {2001.04301},
5252
archiveprefix = {arXiv},
@@ -126,7 +126,7 @@ @inproceedings{unification
126126
@article{carneiro2019type,
127127
title = {The type theory of Lean},
128128
author = {Carneiro, Mario},
129-
journal = {preparation (https://github. com/digama0/lean-type-theory/releases)},
129+
url = {https://github.com/digama0/lean-type-theory/releases},
130130
year = {2019}
131131
}
132132

@@ -142,15 +142,15 @@ @article{schonfinkel1924bausteine
142142
}
143143

144144
@book{curry,
145-
author = {Curry, Haskell B. (Haskell Brooks) and Hindley, J. Roger. and Seldin, J. P.},
146-
address = {London ;},
147-
booktitle = {To H.B. Curry : essays on combinatory logic, lambda calculus, and formalism},
145+
author = {Curry, Haskell and Hindley, J. Roger. and Seldin, Jonathan P.},
146+
address = {London},
147+
booktitle = {Essays on combinatory logic, lambda calculus, and formalism.},
148148
isbn = {0123490502},
149149
keywords = {Curry Haskell B (Haskell Brooks) 1900-1982 ; Logic Symbolic and mathematical ; Logic Symbolic and mathematical Addresses essays lectures},
150150
language = {eng},
151151
lccn = {80040139},
152152
publisher = {Academic Press},
153-
title = {To H.B. Curry : essays on combinatory logic, lambda calculus, and formalism },
153+
title = {Essays on combinatory logic, lambda calculus, and formalism },
154154
year = {1980}
155155
}
156156

@@ -185,8 +185,9 @@ @article{eauto
185185

186186
@book{lambdacalc,
187187
place = {Cambridge},
188-
series = {Perspectives in Logic},
189188
title = {Lambda Calculus with Types},
189+
booktitle = {Lambda Calculus with Types},
190+
series = {Perspectives in Logic},
190191
publisher = {Cambridge University Press},
191192
author = {Barendregt, Henk and Dekkers, Wil and Statman, Richard},
192193
year = {2013},
@@ -195,8 +196,8 @@ @book{lambdacalc
195196

196197
@article{metaprogrammingbook,
197198
title = {Metaprogramming in Lean 4},
198-
author = {Paulino, Arthur and Testa, Damiano and Ayers, Edward and Karunus, Evgenia and Böving, Henrik and Limperg, Jannis and Gadgil, Siddhartha and Bhat, Siddharth},
199-
journal = {preparation (https://leanprover-community.github.io/lean4-metaprogramming-book)},
199+
author = {Paulino, Arthur and Testa, Damiano and Ayers, Edward and Karunus, Evgenia and B{\"o}ving, Henrik and Limperg, Jannis and Gadgil, Siddhartha and Bhat, Siddharth},
200+
url = {https://leanprover-community.github.io/lean4-metaprogramming-book},
200201
year = {2025}
201202
}
202203

0 commit comments

Comments
 (0)