-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
307 lines (235 loc) · 12.3 KB
/
index.html
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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
<!DOCTYPE html>
<html>
<head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Aleš Bizjak</title>
<!-- <meta name="description" content="Postdoctoral researcher at Aarhus University"> -->
<link rel="stylesheet" href="/css/main.css">
<link rel="canonical" href="https://abizjak.github.io/">
</head>
<body>
<header class="site-header">
<div class="wrapper">
<a class="site-title" href="/"> Aleš Bizjak </a>
<div class="site-title" style="margin-left:10px;"> ([email protected])</div>
<nav class="site-nav">
<a href="#" class="menu-icon">
<svg viewBox="0 0 18 15">
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
</svg>
</a>
<div class="trigger">
<a class="page-link" href="/emacs/">Emacs</a>
<a class="page-link" href="/quotes/">Quotes</a>
</div>
</nav>
</div>
</header>
<div class="page-content">
<div class="wrapper">
<p>I am currently a software engineer. Previously I was a postdoctoral researcher at the Department of Computer Science of Aarhus
University where I worked on program logics for concurrency, and semantics of programming languages, logics, and type theories.</p>
<p><a href="https://scholar.google.dk/citations?user=7MZ1pfoAAAAJ">Google Scholar</a>
|
<a href="http://dblp.uni-trier.de/pers/hd/b/Bizjak:Ales">DBLP</a>
|
<a href="http://github.com/abizjak"> Github </a>
<!-- <h1 id="drafts">Drafts</h1> -->
<h1 id="publications">Publications</h1>
<ul>
<li>
<p><a href="https://doi.org/10.1017/S0960129520000080">Denotational semantics for guarded dependent type theory</a><br />
<em>Aleš Bizjak and Rasmus Ejlers Møgelberg</em><br />
<a href="https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/issue/5C1EA82251348B2E15210CDDB0E5E4B1">
Mathematical Strucures in Computer Science, Vol 30, Issue 4</a><br />
<a href="https://arxiv.org/abs/1802.03744">ArXiv preprint</a></p>
</li>
<li>
<p><a href="https://dl.acm.org/doi/10.1145/3290378">Iron: Managing Obligations in Higher-Order Concurrent Separation Logic</a><br />
<em>Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal</em><br />
<a href="https://popl19.sigplan.org/">POPL 2019</a><br />
<a href="https://iris-project.org/iron/">Preprint and Coq formalization</a></p>
</li>
<li>
<p><a href="https://doi.org/10.1007/s10817-018-9471-7">Guarded Cubical Type Theory</a><br />
<em>Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi</em><br />
Journal of Automated Reasoning, Special Issue on Homotopy Type Theory and Univalent Foundations, 2018
(extended version of the CSL’16 paper)<br />
<a href="https://arxiv.org/abs/1611.09263">ArXiv preprint</a></p>
</li>
<li>
<p><a href="https://doi.org/10.1016/j.tcs.2018.02.012">A Model of Guarded Recursion via Generalised Equilogical Spaces</a><br />
<em>Aleš Bizjak and Lars Birkedal</em><br />
<a href="https://www.journals.elsevier.com/theoretical-computer-science/">TCS</a><br />
<a href="/documents/drafts/guarded-equilogical-submitted.pdf">PDF (preprint)</a></p>
</li>
<li>
<p><a href="https://doi.org/10.1007/978-3-319-89884-1_8">Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus</a><br />
<em>Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Aleš Bizjak, Marco Gaboardi, and Deepak Garg</em><br />
ESOP 2018<br />
<a href="https://arxiv.org/abs/1802.09787">ArXiv preprint</a></p>
</li>
<li>
<p><a href="http://dx.doi.org/10.1017/S0956796818000151">Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic</a><br />
<em>Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer</em><br />
<a href="http://dx.doi.org/10.1017/S0956796818000151">JFP</a><br />
<a href="/documents/publications/iris-ground-up.pdf">PDF (preprint)</a></p>
</li>
<li>
<p><a href="https://doi.org/10.1016/j.entcs.2018.03.016">On Models of Higher-Order Separation Logic</a><br />
<em>Aleš Bizjak and Lars Birkedal</em><br />
MFPS 2017<br />
<a href="/documents/publications/box-modality-mfps.pdf">Preprint</a></p>
</li>
<li>
<p>The Essence of Higher-Order Concurrent Separation Logic<br />
<em>Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal</em><br />
ESOP 2017<br />
<a href="http://iris-project.org/pdfs/2017-esop-iris3-final.pdf">Preprint</a></p>
</li>
<li>
<p><a href="http://arxiv.org/abs/1606.05223">Guarded Cubical Type Theory: Path Equality for Guarded Recursion</a><br />
<em>Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi</em><br />
CSL 2016<br />
<a href="http://arxiv.org/abs/1606.05223">ArXiv preprint</a></p>
</li>
<li>
<p><a href="http://arxiv.org/abs/1606.09455">The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types</a><br />
<em>Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal</em><br />
Logical Methods in Computer Science <a href="https://lmcs.episciences.org/2019">special issue</a>
(journal version of FoSSaCS’15 paper).<br />
<a href="http://arxiv.org/abs/1606.09455">ArXiv</a></p>
</li>
<li>
<p><a href="http://arxiv.org/abs/1601.01586">Guarded Dependent Type Theory with Coinductive Types</a><br />
<em>Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Rasmus Ejlers Møgelberg, and Lars Birkedal</em><br />
FoSSaCS 2016<br />
<a href="http://arxiv.org/abs/1601.01586">ArXiv preprint</a></p>
</li>
<li>
<p><a href="http://link.springer.com/chapter/10.1007/978-3-319-22102-1_25">ModuRes: a Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages</a><br />
<em>Filip Sieczkowski, Aleš Bizjak, and Lars Birkedal</em><br />
ITP 2015<br />
<a href="/documents/publications/modures-library-itp.pdf">Preprint</a></p>
</li>
<li>
<p><a href="http://dx.doi.org/10.1016/j.entcs.2015.12.007">A model of guarded recursion with clock synchronisation</a><br />
<em>Aleš Bizjak and Rasmus Ejlers Møgelberg</em><br />
MFPS 2015</p>
</li>
<li>
<p><a href="http://link.springer.com/chapter/10.1007/978-3-662-46678-0_18">Step-Indexed Logical Relations for Probability</a><br />
<em>Aleš Bizjak and Lars Birkedal</em><br />
FoSSaCS 2015<br />
<a href="http://arxiv.org/abs/1501.02623">ArXiv preprint</a></p>
</li>
<li>
<p><a href="http://link.springer.com/chapter/10.1007/978-3-662-46678-0_26">Programming and Reasoning with Guarded Recursion for Coinductive Types</a><br />
<em>Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal</em><br />
FoSSaCS 2015<br />
<a href="http://arxiv.org/abs/1501.02925">ArXiv preprint</a></p>
</li>
<li>
<p><a href="http://link.springer.com/chapter/10.1007/978-3-319-08918-8_8">A Model of Countable Nondeterminism in Guarded Type Theory</a><br />
<em>Aleš Bizjak, Lars Birkedal, and Marino Miculan</em><br />
RTA-TLCA 2014<br />
<a href="/documents/publications/countable-nondet-internal-tlca.pdf">Preprint</a>
|
<a href="/documents/trs/cntbl-gtt-tr.pdf">Technical report</a></p>
</li>
<li>
<p><a href="http://arxiv.org/abs/1310.2031">Step-Indexed Relational Reasoning for Countable Nondeterminism</a> <br />
<em>Lars Birkedal, Aleš Bizjak, and Jan Schwinghammer</em> <br />
Logical Methods in Computer Science, Volume 9, Issue 4, 2013<br />
<a href="http://arxiv.org/abs/1310.2031">ArXiv preprint</a></p>
</li>
</ul>
<h1 id="phd-thesis">PhD thesis</h1>
<ul>
<li><a href="/documents/thesis/semantics-applications-gr.pdf">On Semantics and Applications of Guarded Recursion</a><br />
Aarhus University, 2016</li>
</ul>
<h1 id="notes-and-tutorials">Notes and tutorials</h1>
<ul>
<li>
<p>Some theorems about mutually recursive domain equations in the category of preordered COFEs
<em>Aleš Bizjak</em><br />
<a href="/documents/notes/mutually-recursive-domain-eq.pdf">PDF</a></p>
</li>
<li>
<p>A Taste of Categorical Logic - Tutorial Notes<br />
<em>Aleš Bizjak and Lars Birkedal</em><br />
<a href="/documents/publications/categorical-logic-tutorial-notes.pdf">PDF</a></p>
</li>
<li>
<p>A note on the transitivity of step-indexed logical relations<br />
<em>Lars Birkedal and Aleš Bizjak</em><br />
<a href="/documents/notes/step-indexed-transitivity.pdf">PDF</a></p>
</li>
</ul>
<h1 id="service">Service</h1>
<ul>
<li>
<p><a href="https://popl19.sigplan.org/">POPL 2019</a> artifact evaluation committee member</p>
</li>
<li>
<p><a href="https://icfp18.sigplan.org/track/hope-2018-papers">HOPE 2018</a> program committee member</p>
</li>
<li>
<p><a href="https://conf.researchr.org/home/icfp-2018/">ICFP 2018</a> artifact evaluation committee member</p>
</li>
<li>
<p><a href="https://www.mathstat.dal.ca/mfps2018/">MFPS 2018</a> program committee member</p>
</li>
<li>
<p><a href="https://lmcs.episciences.org/">LMCS</a> layout editor</p>
</li>
<li>
<p><a href="https://popl18.sigplan.org/">POPL 2018</a> artifact evaluation committee member</p>
</li>
<li>
<p><a href="https://popl17.sigplan.org/">POPL 2017</a> artifact evaluation committee member</p>
</li>
</ul>
<h1 id="software">Software</h1>
<p>Occasionally I write some software, some of which you might find useful, hence I
list it here. My Github account is <a href="http://github.com/abizjak">here</a>.</p>
<h2 id="alg-a-program-for-enumerating-models-of-algebraic-theories"><a href="https://github.com/andrejbauer/alg">Alg</a>, a program for enumerating models of algebraic theories</h2>
<p>Alg is a program for enumeration of finite models of single-sorted first-order
theories. Such a theory is given by a signature (a list of constants,
operations and relations) and axioms expressed in first-order logic. Examples
of first-order theories include groups, lattices, rings, fields, posets,
graphs, and many others. Alg can do the following:</p>
<ul>
<li>list or count all non-isomorphic models of a given theory,</li>
<li>list or count all non-isomorphic indecomposable models of a given theory.</li>
</ul>
<p>Written together with <a href="http://andrej.com">Andrej Bauer</a>. The source is on
<a href="https://github.com/andrejbauer/alg">Github</a> and we have also written a
<a href="/documents/publications/alg-manual.pdf">manual</a>.</p>
<h2 id="a-turing-machine-simulator">A Turing machine simulator</h2>
<p>A very simple Turing machine simulator written for
use in a course for second year undergraduate students.
Written in Haskell and compiled to Javascript with the
<a href="https://github.com/valderman/haste-compiler">Haste</a> compiler.</p>
<p><a href="https://abizjak.github.io/turingjs/turingjs.html">Here</a> you can see it running.
The source is available on <a href="https://bitbucket.org/abizjak/turingjs">Bitbucket</a>.</p>
<h2 id="another-turing-machine-simulator-and-compiler">Another Turing machine simulator and compiler</h2>
<p>A more sophisticated Turing machine simulator with a proper parser and syntax
for defining them. It also allows writing multi-tape Turing machines and
running them. Part of the project is also a compiler from a simple variant of
call-by-value λ-calculus to 5-tape Turing machines with a few examples showing
how the compiled Turing machine computes the given function.</p>
<p>The source, with examples and more details, is on <a href="https://bitbucket.org/abizjak/turing">Bitbucket</a>.</p>
</div>
</div>
<footer class="site-footer">
<div class="wrapper">
</div>
</footer>
</body>
</html>