-
Notifications
You must be signed in to change notification settings - Fork 0
/
refs.bib
156 lines (150 loc) · 4.94 KB
/
refs.bib
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
@phdthesis{norell:thesis,
author = {Ulf Norell},
title = {Towards a practical programming language based on dependent type
theory},
school = {Department of Computer Science and Engineering, Chalmers University of Technology},
year = 2007,
month = {September},
address = {SE-412 96 G\"{o}teborg, Sweden}
}
@article{two-new-series,
title = {Two New Series of Principles in the Interpretability Logic of All Reasonable Arithmetical Theories},
volume = {85},
number = {1},
journal = {Journal of Symbolic Logic},
pages = {1--25},
author = {Evan Goris and Joost J. Joosten},
doi = {10.1017/jsl.2019.90},
year = {2020}
}
@article{Mikec-Vukovic-20,
author = "L. Mikec and M. Vuković",
title = "Interpretability logics and generalised {V}eltman semantics",
journal = "Accepted for publication in The Journal of Symbolic Logic",
url = {https://arxiv.org/abs/1907.03849 (preprint version)},
year = {to appear},
}
@article{modal-matters,
author = {Goris, E. and Joosten, J. J.},
title = "{Modal Matters for Interpretability Logics}",
journal = {Logic Journal of the IGPL},
volume = {16},
number = {4},
pages = {371-412},
year = {2008},
month = {08},
issn = {1367-0751},
doi = {10.1093/jigpal/jzn013},
url = {https://doi.org/10.1093/jigpal/jzn013},
eprint = {https://academic.oup.com/jigpal/article-pdf/16/4/371/2055430/jzn013.pdf},
}
@article{agda-stdlib,
title={The Agda standard library},
author={Danielsson, Nils Anders and Norell, Ulf and Mu, SC and Bronson, S and
Doel, D and Jansson, P and Chen, LT et al},
url={https://github.com/agda/agda-stdlib},
year={2020}
}
@Book{plfa2019,
author = {Philip Wadler and Wen Kokke},
title = {Programming Language Foundations in {A}gda},
note = {Available at \url{http://plfa.inf.ed.ac.uk/}},
year = 2019,
}
@misc{agda-doc,
title = {Agda's documentation},
year = 2020,
howpublished = "\url{https://agda.readthedocs.io/en/latest/}"
}
@mastersthesis{joosten-master,
author = "J.J. Joosten",
title = "Towards the interpretability logic of all reasonable arithmetical
theories",
school = "University of Amsterdam",
year = "1998"}
@unpublished{Verbrugge,
author="Verbrugge, L.C.",
title ={Verzamelingen-Veltman frames en modellen (Set Veltman frames and models)},
note ={Unpublished manuscript},
year ={1992}}
@article{a-new-principle,
author = {Goris, E. and Joosten, J. J.},
title = {A new principle in the interpretability logic of all
reasonable arithmetical theories},
journal = {Logic Journal of the IGPL},
fjournaL = {Logic Journal of the IGPL. Interest Group in Pure and Applied Logics},
volume = {19},
year = {2011},
number = {1},
pages = {14--17}
}
@phdthesis{interpretability-formalized,
author={Joosten, J. J.},
title={Interpretability Formalized},
school={Utrecht University},
publisher={Department of Philosophy, University of Utrecht},
isbn={90-393-3869-8},
year={2004},
}
@article{wadler2015propositions,
title={Propositions as types},
author={Wadler, Philip},
journal={Communications of the ACM},
volume={58},
number={12},
pages={75--84},
year={2015},
publisher={ACM New York, NY, USA}
}
@mastersthesis{MasRovira:2020:MastersThesis,
author={Mas Rovira, J.},
title={{I}nterpretability {L}ogics and {G}eneralised {V}eltman {S}emantics in {A}gda},
school={Master in Pure and Applied Logic, University of Barcelona},
organization={University of Barcelona},
year={forthcoming, 2020},
url={http://diposit.ub.edu/dspace/handle/2445/133559},
}
@article{GorisJoosten:2011:ANewPrinciple,
AUTHOR = {Goris, E. and Joosten, J.J.},
TITLE = {A new principle in the interpretability logic of all
reasonable arithmetical theories},
JOURNAL = {Logic Journal of the IGPL},
FJOURNAL = {Logic Journal of the IGPL. Interest Group in Pure and Applied Logics},
VOLUME = {19},
YEAR = {2011},
NUMBER = {1},
PAGES = {14--17},
}
@book{martin1984intuitionistic,
title={Intuitionistic type theory},
author={Martin-L{\"o}f, Per and Sambin, Giovanni},
volume={9},
year={1984},
publisher={Bibliopolis Naples}
}
@misc{agda:universe-levels,
title ={Agda documentation on universe levels},
author= {},
url = "https://agda.readthedocs.io/en/latest/language/universe-levels.html",
year = "2020"
}
@InCollection{JaparidzeJongh:1998:HandbookPaper,
author = "Japaridze, G. and {de} Jongh, D.",
title = "The logic of provability",
booktitle = "Handbook of proof theory",
publisher = "North-Holland Publishing Co.",
year = "1998",
editor = "Buss, S.",
pages = "475--546",
OPTaddress = "",
address = "Amsterdam"
}
@misc{joosten2020overview,
title={An overview of Generalised Veltman Semantics},
author={Joost J. Joosten and Jan Mas Rovira and Luka Mikec and Mladen Vuković},
year={2020},
eprint={2007.04722},
url={https://arxiv.org/abs/2007.04722}
archivePrefix={arXiv},
primaryClass={math.LO}
}