forked from michaelt/martin-lof
-
Notifications
You must be signed in to change notification settings - Fork 0
/
bibliography.bib
148 lines (134 loc) · 4.57 KB
/
bibliography.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
@InProceedings{martinlof1971hauptsatz,
Title = {Hauptsatz for the intuitionistic theory of iterated
inductive definitions},
Author = {Martin-L{\"o}f, Per},
Booktitle = {Proceedings of the 2nd Scandinavian logic symposium},
Year = 1971,
Editor = {Fenstad, Jan Erik},
Publisher = {North-Holland},
Series = {Studies in Logic and the Foundations of Mathematics},
Volume = {63},
Pages = {179 -- 216},
}
@incollection{Martin-Lof-1972,
Author = {Martin-L{\"o}f, Per},
Booktitle = {Twenty-five years of constructive type theory ({V}enice, 1995)},
Mrclass = {03B15 (03F55)},
Mrnumber = 1686864,
Pages = {127--172},
Publisher = {Oxford University Press},
Editor = {Giovanni Sambin and Jan M. Smith},
Series = {Oxford Logic Guides},
Title = {An intuitionistic theory of types},
Volume = 36,
Year = 1998}
@incollection{Martin-Lof-1973,
Author = {Martin-L{\"o}f, Per},
Booktitle = {Logic Colloquium '73, Proceedings of the Logic Colloquium},
Editor = {H.E. Rose and J.C. Shepherdson},
Mrclass = {02C15 (02D99)},
Mrnumber = {0387009 (52 \#7856)},
Mrreviewer = {Horst Luckhardt},
Pages = {73--118},
Publisher = {North-Holland},
Series = {Studies in Logic and the Foundations of Mathematics},
Title = {An intuitionistic theory of types: predicative part},
Volume = 80,
Year = 1975}
@TechReport{hml75,
author = {Hancock, Peter and Martin-L\"{o}f, Per},
title = {Syntax and semantics of the language of primitive
recursive functions},
institution = {University of Stockholm},
year = 1975,
number = 3,
address = {Stockholm, Sweden}
}
@incollection{Martin-Lof-1979,
Author = {Martin-L{\"o}f, Per},
Booktitle = {Logic, Methodology and Philosophy of Science VI, Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover 1979},
Editor = {L. Jonathan Cohen and Jerzy {Łoś} and Helmut Pfeiffer and Klaus-Peter Podewski},
Doi = {10.1016/S0049-237X(09)70189-2},
Mrclass = {03F50 (03B70 03F55 68Q45)},
Mrnumber = {682410 (85d:03112)},
Mrreviewer = {B. H. Mayoh},
Pages = {153--175},
Publisher = {North-Holland},
Series = {Studies in Logic and the Foundations of Mathematics},
Title = {Constructive mathematics and computer programming},
Url = {http://dx.doi.org/10.1016/S0049-237X(09)70189-2},
Volume = 104,
Year = 1982}
@book{martin-lof:bibliopolis,
Author = {Martin-L{\"o}f, Per},
Isbn = {88-7088-105-9},
Mrclass = {03B15 (03F50 03F55)},
Mrnumber = {769301 (86j:03005)},
Mrreviewer = {M. M. Richter},
Pages = {iv+91},
Publisher = {Bibliopolis},
Series = {Studies in Proof Theory},
Subtitle = {Notes by Giovanni Sambin},
Title = {Intuitionistic type theory},
Volume = {1},
Year = {1984}}
@article{martin2006100,
Author = {Martin-L{\"o}f, Per},
Journal = {The Computer Journal},
Number = {3},
Pages = {345--350},
Publisher = {BCS},
Title = {100 years of {Z}ermelo's axiom of choice: what was the problem with it?},
Volume = {49},
Year = {2006}}
@article{martin1996meanings,
title={On the meanings of the logical constants and the justifications of the logical laws},
author={Martin-L{\"o}f, Per},
journal={Nordic journal of philosophical logic},
volume={1},
number={1},
pages={11--60},
year={1996}
}
@article{martin1987truth,
title={Truth of a proposition, evidence of a judgement, validity of a proof},
author={Martin-L{\"o}f, Per},
journal={Synthese},
pages={407--420},
year={1987},
publisher={JSTOR}
}
@misc{martinlof1993leiden,
author = "Per Martin-L{\"o}f",
title = "Philosophical aspects of intuitionistic type theory",
year={1993},
URL = {https://pml.flu.cas.cz/uploads/PML-LeidenLectures93.pdf},
note={Transcriptions of lectures given at Leiden University from 23 September to 16 December 1993},
}
@article{martinlof2021sense,
title = {The Sense/Reference Distinction in Constructive Semantics},
volume = {27},
pages = {501--513},
journal = {Bulletin of Symbolic Logic},
author = {Per Martin-L\"{o}f},
number = {4},
year = {2021},
note={Transcription of a talk given at Leiden University on 25 August, 2001},
URL = {https://doi.org/10.1017/bsl.2021.61},
}
@incollection{martin2013verificationism,
title={Verificationism then and now},
author={Martin-L{\"o}f, Per},
booktitle={Judgement and the Epistemic Foundation of Logic},
pages={3--14},
year={2013},
publisher={Springer}
}
@incollection{martin1994analytic,
title={Analytic and synthetic judgements in type theory},
author={Martin-L{\"o}f, Per},
booktitle={Kant and contemporary epistemology},
pages={87--99},
year={1994},
publisher={Springer}
}