-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathindex.html
More file actions
executable file
·870 lines (841 loc) · 46.4 KB
/
index.html
File metadata and controls
executable file
·870 lines (841 loc) · 46.4 KB
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
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
<!DOCTYPE HTML>
<!--
Strongly Typed 1.1 by HTML5 UP
html5up.net | @n33co
Free for personal and commercial use under the CCA 3.0 license (html5up.net/license)
-->
<html>
<head>
<title>Paul Downen</title>
<meta http-equiv="content-type" content="text/html; charset=utf-8" />
<meta name="description" content="" />
<meta name="keywords" content="" />
<meta name="viewport" content="width=1040" />
<link href="http://fonts.googleapis.com/css?family=Source+Sans+Pro:300,400,600|Arvo:700" rel="stylesheet" type="text/css" />
<!--[if lte IE 8]><script src="js/html5shiv.js"></script><![endif]-->
<script src="js/jquery.min.js"></script>
<script src="js/jquery.dropotron.min.js"></script>
<script src="js/config.js"></script>
<script src="js/skel.min.js"></script>
<script src="js/skel-panels.min.js"></script>
<noscript>
<link rel="stylesheet" href="css/skel-noscript.css" />
<link rel="stylesheet" href="css/style.css" />
<link rel="stylesheet" href="css/style-desktop.css" />
</noscript>
</head>
<body class="no-sidebar">
<!-- Header Wrapper -->
<div id="header-wrapper">
<!-- Header -->
<div id="header" class="container">
<!-- Logo -->
<h1 id="logo"><a href="#">Paul Downen</a></h1>
<p>
Miner School of Computer & Information Sciences,
<br />
University of Massachusetts, Lowell.
</p>
<!-- Nav -->
<nav id="nav">
<ul>
<!-- <li><a class="fa fa-home" href="index.html"><span>Introduction</span></a></li> -->
<li><a class="fa fa-terminal" href="#research"><span>Research</span></a></li>
<li><a class="fa fa-pencil" href="#teaching"><span>Teaching</span></a></li>
<li>
<a class="fa fa-quote-left" href="#publications"><span>Publications</span></a>
<ul>
<li><a href="#journal-articles">Journal Articles</a></li>
<li><a href="#conference-papers">Conference and Workshops</a></li>
<li><a href="#unpublished-manuscripts">Unpublished Manuscripts</a></li>
</ul>
</li>
<li>
<a class="fa fa-comment" href="#presentations"><span>Presentations</span></a>
<ul>
<li><a href="#conference-talks">Conference Talks</a></li>
<li><a href="#workshop-talks">Workshop Talks</a></li>
<li><a href="#invited-talks">Invited Talks</a></li>
<li><a href="#oplss">OPLSS</a></li>
</ul>
</li>
<li><a class="fa fa-envelope" href="#contact"><span>Contact</span></a></li>
</ul>
</nav>
</div>
</div>
<!-- Main Wrapper -->
<div id="main-wrapper">
<!-- Main -->
<div id="main" class="container">
<div class="row">
<!-- Content -->
<div id="content" class="12u skel-cell-important">
<!-- Post -->
<article class="is-post" id="about">
<p>
I am an Assistant Professor in the <a href="https://cs.uml.edu">Miner School of Computer & Information Sciences</a> at <a href="https://www.uml.edu/">University of Massachusetts, Lowell</a> since Fall 2021.
<!--
<br />
<b>I'm currently looking for motivated students to work with! If you're interested, send me a <a href="mailto:paul@pauldownen.com">message</a>.</b>
-->
</p>
<p>
Previously, I completed my Ph.D. from the <a href="https://www.uoregon.edu/">University of Oregon</a>'s <a href="https://cs.uoregon.edu/">Department of Computer and Information Science</a>.
</p>
</article>
<!-- Post -->
<article class="is-post" id="research">
<header>
<a href="#"><h2>Research Interests</h2></a>
</header>
<p>
My general research interests are in the study of <em>programming languages</em>, including their <em>theory</em>, <em>semantics</em>, <em>design</em>, and <em>implementation</em>, with a focus on the <em>foundations of computation</em> and its relation to <em>logic</em> and <em>duality</em>.
In particular, I am interested in using logic to help <em>verify</em> that software systems and their <em>compilation</em> is <em>efficient</em>, <em>correct</em>, <em>safe</em>, and <em>secure</em>.
I'm also interested in aspects of practical languages including <em>computational effects</em> (like mutable state, exceptions, and first-class continuations) and ways for languages to sensibly bridge between <em>high-level abstractions</em> and <em>low-level implementation details</em>.
</p>
<p>
I have worked on an alternative model for computation based on the connection between programming languages and formal logic (known as the Curry-Howard correspondence or proofs-as-programs interpretation).
With a single stroke in 1935, Gentzen laid out the basis for the modern study of formalized logic: <em>natural deduction</em> and the <em>sequent calculus</em>. On the one hand, natural deduction is the logic of the lambda calculus, which serves as the bedrock for functional programming languages (like Scheme, Haskell, and OCaml) and proof assistants (like Coq).
On the other hand, the sequent calculus has only recently been connected with a lower-level model for programs that highlights the dualities present in programming languages and details such as evaluation strategies (like strict or lazy evaluation) and control-flow effects (like exceptions).
I am developing this model of computation to get another view of programs and languages from different angles:
<ul>
<li class="fa fa-angle-right">
A high-level calculus for reasoning about the behavior of programs (in a similar style as the lambda calculus) while also accounting for low-level details such as evaluation strategy and control flow.
</li>
<li class="fa fa-angle-right">
A contextual representation of programs that allows for performing context-sensitive analysis and transformation of programs, as done by optimizing compilers like the <a href="https://www.haskell.org/ghc/">Glasgow Haskell Compiler (GHC)</a>.
</li>
<li class="fa fa-angle-right">
A dualized framework that gives a symmetric and unified view of programming concepts, as a way to understand differences and similarities in language design, including types and abstraction mechanisms from both functional and object-oriented languages.
</li>
</ul>
</p>
<p>
Some of these ideas have been (or are currently being) implemented inside GHC for analyzing and optimizing Haskell programs.
<ul>
<li class="fa fa-angle-right">
<a href="https://hackage.haskell.org/package/sequent-core">Sequent Core</a> (based on <a href="publications/scfp.pdf">"Sequent Calculus as a Compiler Intermediate Language"</a>) is a plugin for GHC that replaces its Core intermediate language with an alternative one based on the sequent calculus.
</li>
<li class="fa fa-angle-right">
<a href="https://github.com/lukemaurer/ghc/tree/wip/join-points">Join points</a> (based on <a href="publications/pldi17.pdf">"Compiling Without Continuations"</a>) are an extension to the GHC Core language with purely functional labels and jumps, used to optimize branching control flow in programs.
</li>
<li class="fa fa-angle-right">
Static calling conventions (based on <a href="publications/kacc.pdf">"Kinds Are Calling Conventions"</a>) are a type-based approach to integrating parametric polymorphism with C-like function calls, including number of arguments and their machine representations, completely at compile-time.
</li>
</ul>
</p>
</article>
<article class="is-post" id="teaching">
<header>
<a href="#"><h2>Teaching</h2></a>
</header>
Courses I have taught at University of Massachusetts, Lowell:
<ul>
<li class="fa fa-angle-double-right">
<a href="courses/26S/EFP/index.html">
Spring 2026: <b>COMP.4600/5300</b> <i>Effective Functional Programming</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/25F/OPL/index.html">
Fall 2025: <b>COMP.3010</b> <i>Organization of Programming Languages</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/25S/Logic/index.html">
Spring 2025: <b>COMP.4600/5300</b> <i>Logic, Programs & Verification</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/24F/Assembly/index.html">
Fall 2024: <b>COMP.2030</b> <i>Assembly Language Programming</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/24S/Assembly/index.html">
Spring 2024: <b>COMP.2030</b> <i>Assembly Language Programming</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/23F/EFP/index.html">
Fall 2023: <b>COMP.4600/5300</b> <i>Effective Functional Programming</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/23F/Assembly/index.html">
Fall 2023: <b>COMP.2030</b> <i>Assembly Language Programming</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/23S/OPL/index.html">
Spring 2023: <b>COMP.3010</b> <i>Organization of Programming Languages</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/22F/EFP/index.html">
Fall 2022: <b>COMP.4600/5300</b> <i>Effective Functional Programming</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/22U/OPL/index.html">
Summer 2022: <b>COMP.3010</b> <i>Organization of Programming Languages</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/22S/OPL/index.html">
Spring 2022: <b>COMP.3010</b> <i>Organization of Programming Languages</i>.
</a>
</li>
<li class="fa fa-angle-double-right">
<a href="courses/21F/EFP/index.html">
Fall 2021: <b>COMP.5300</b> <i>Effective Functional Programming</i>.
</a>
</li>
</ul>
<br />
My teaching at the University of Oregon was focused on the theory and practice of programming languages, and how it helps us write better software.
Previous courses I have designed and taught include:
<ul>
<li class="fa fa-angle-double-right">
<i>Foundations of Programming Languages</i>, an intensive introduction to the fundamentals of the theory of programming languages, for graduate students, advanced undergraduate students, and interested experts from other fields.
This course was given at the Oregon Programming Languages Summer School <a href="https://www.cs.uoregon.edu/research/summerschool/summer17/topics.php#review">2017</a> and <a href="https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php#review">2018</a>.
</li>
<br />
<li class="fa fa-angle-double-right">
<i>Advanced Functional Programming</i>, an application of advanced topics and techniques of functional programming for writing practical, interactive, and correct software.
This course was given in <a href="https://classes.cs.uoregon.edu/18S/cis410afp/">Spring 2018</a>.
</li>
</ul>
<br />
I have also given lectures on the application of numerical methods with functional programming in Python, based on John Hughes' fantastic paper "<a href="https://www.cs.kent.ac.uk/people/staff/dat/miranda/whyfp90.pdf">Why Functional Programming Matters</a>."
<br />
<ul>
<li class="fa fa-angle-double-right">
<a href="notes/nmfp.pdf">Lecture notes</a>
</li>
<li class="fa fa-angle-double-right">
Accompanying <a href="notes/nmfp_template.py">Python template</a>
</li>
</ul>
</article>
<article class="is-post" id="publications">
<header>
<a href="#"><h2>Publications</h2></a>
</header>
<h3 id="journal-articles">Journal Articles</h3>
<ul>
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2025).
<b>A Contextual Formalization of Structural Coinduction</b>.
<i>Journal of Functional Programming</i>.
<br />
<a href="https://doi.org/10.1017/S0956796825100026">(doi)</a>
<a href="publications/coind-proof.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2023).
<b>Classical (Co)Recursion: Mechanics</b>.
<i>Journal of Functional Programming</i>, Volume 33, e4.
<br />
<a href="https://doi.org/10.1017/S0956796822000168">(doi)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2020).
<b>Compiling With Classical Connectives</b>.
<i>Logical Methods in Computer Science</i>, Volume 16, Issue 3, pp. 13:1-13:57.
<br />
<a href="publications/1907.13227.pdf">(pdf)</a>
<a href="https://lmcs.episciences.org/6740">(online)</a>
<a href="https://arxiv.org/abs/1907.13227">(arXiv)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Zena M. Ariola, and Silvia Ghilezan. (2019).
<b>The duality of classical intersection and union types</b>.
<i>Fundamenta Informaticae</i>, 170, 2019.
<br />
<a href="publications/interunion.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. (2019).
<b>Abstracting models of strong normalization for classical calculi</b>.
<i>Journal of Logical and Algebraic Methods in Programming</i>, 2019.
<br />
<a href="publications/classical-sn.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2018).
<b>A Tutorial on Computational Classical Logic and the Sequent Calculus</b>.
<i>Journal of Functional Programming</i>, 28, e3.
<br />
<a href="https://doi.org/10.1017/S0956796818000023">(doi)</a>
<a href="publications/sequent-intro.pdf">(pdf+appendix)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. (2017).
<b>Call-by-Name Extensionality and Confluence</b>.
<i>Journal of Functional Programming</i>, 27, e12.
<br />
<a href="https://doi.org/10.1017/S095679681700003X">(doi)</a>
<a href="publications/surjective-call-stacks.pdf">(pdf+appendix)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. (2016).
<b>First class call stacks: Exploring head reduction</b>.
In <i>Olivier Danvy and Ugo de'Liguoro: Proceedings of the Workshop on Continuations, London, UK, (WoC2015), Electronic Proceedings in Theoretical Computer Science</i>, 212, pp. 18–35.
<br />
<a href="http://arxiv.org/abs/1606.06378">(arXiv)</a>
<a href="publications/first-class-call-stacks.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2014).
<b>Delimited control and computational effects</b>.
<i>Journal of Functional Programming</i>, 24, pp 1-55.
<br />
<a href="https://dx.doi.org/10.1017/S0956796813000312">(doi)</a>
<a href="publications/delimited-control-effects.pdf">(pdf+appendix)</a>
</li>
</ul>
<h3 id="conference-papers">Conference Papers</h3>
<ul>
<li class="fa fa-angle-double-right">
Paul Downen. (2025).
<b>Controling Copatterns: There and Back Again</b>.
In <i>OlivierFest 2025</i>.
<br />
<a href="publications/derive-copat.pdf">(pdf)</a>
<a href="https://github.com/pdownen/derive-copat">(github)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen. (2025).
<b>Rewriting Macros on the Fly: A Modular Approach to Administrative Reduction During Expansion</b>.
In <i>Scheme 2025</i>.
<br />
<a href="publications/rewrite-macros.pdf">(pdf)</a>
<a href="https://github.com/pdownen/rewrite-macros">(github)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2025).
<b>CoScheme: Compositional Copatterns in Scheme</b>.
In <i>Trends in Functional Programming (TFP2025)</i>.
<b>Best Paper Award</b> nominee.
<br />
<a href="publications/coscheme.pdf">(pdf)</a>
<a href="https://github.com/pdownen/CoScheme">(github)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen. (2024).
<b>Call-By-Unboxed-Value</b>.
In <i>International Conference on Functional Programming (ICFP2024)</i>.
<br />
<a href="publications/cbuv.pdf">(pdf)</a>
<a href="https://doi.org/10.1145/3674654">(doi)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Zachary J. Sullivan, Paul Downen, and Zena M. Ariola. (2023).
<b>Closure Conversion in Little Pieces</b>.
In <i>Principles and Practice of Declarative Programming (PPDP2023)</i>.
<br />
<a href="publications/cbpvcc.pdf">(pdf)</a>
<a href="https://doi.org/10.1145/3610612.3610622">(doi)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen. (2022).
<b>Introduction and elimination, left and right</b>.
In <i>International Conference on Functional Programming (ICFP2022)</i>.
<br />
<a href="https://doi.org/10.1145/3547637">(doi)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Zachary J. Sullivan, Paul Downen, and Zena M. Ariola. (2021).
<b>Strictly Capturing Non-strict Closures</b>.
In <i>Partial Evaluation and Program Manipulation (PEPM2021)</i>.
<br />
<a href="https://doi.org/10.1145/3441296.3441398">(doi)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2021). <b>Duality In Action</b>.
In <i>Formal Structures for Computation and Deduction (FSCD2021)</i>.
<br />
<a href="https://doi.org/10.4230/LIPIcs.FSCD.2021.1">(doi)</a>
<a href="publications/dia.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2020).
<b>A Computational Understanding of Classical (Co)Recursion</b>.
In <i>Principles and Practice of Declarative Programming (PPDP2020)</i>.
<br />
<a href="https://doi.org/10.1145/3414080.3414086">(doi)</a>
<a href="publications/corec.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg. (2020). <b>Kinds Are Calling Conventions</b>.
In <i>International Conference on Functional Programming (ICFP2020)</i>.
<br />
<a href="https://doi.org/10.1145/3408986">(doi)</a>
<a href="publications/kacc.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. (2019). <b>Making a Faster Curry with Extensional Types</b>.
In <i>Haskell Symposium, Berlin, Germany (Haskell2019)</i>.
<br />
<a href="publications/eta.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. (2019). <b>Codata in action</b>.
In <i>European Symposium on Programming, Prague, Czech Republic (ESOP2019)</i>.
<br />
<a href="publications/esop2019.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2018). <b>Beyond Polarity: Towards A Multi-Discipline Intermediate Language with Sharing</b>.
In <i>Computer Science Logic, Birmingham, UK (CSL2018)</i>.
<br />
<a href="https://dx.doi.org/10.4230/LIPIcs.CSL.2018.21">(doi)</a>
<a href="publications/csl18_short.pdf">(pdf)</a>
<a href="publications/csl18_long.pdf">(pdf+appendix)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. (2018). <b>Uniform Strong Normalization for Multi-Discipline Calculi</b>.
In <i>International Workshop on Rewriting Logic and its Applications, Thessaloniki, Greece (WRLA2018)</i>.
<br />
<a href="publications/wrla18.pdf">(pdf+appendix)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. (2017). <b>Compiling without Continuations</b>.
In <i>Programming Language Design and Implementation, Barcelona, Spain (PLDI2017)</i>.
<b>Best Paper Award</b>.
<br />
<a href="http://dl.acm.org/authorize?N30138">(acm)</a>
<a href="https://doi.org/10.1145/3062341.3062380">(doi)</a>
<a href="publications/pldi17.pdf">(pdf)</a>
<a href="publications/pldi17_appendix.pdf">(pdf+appendix)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Luke Maurer, Zena Ariola, and Simon Peyton Jones. (2016). <b>Sequent calculus as a compiler intermediate language</b>.
<i>International Conference on Functional Programming, Nara, Japan (ICFP2016)</i>.
<br />
<a href="http://dl.acm.org/authorize?N30137">(acm)</a>
<a href="https://doi.org/10.1145/2951913.2951931">(doi)</a>
<a href="publications/scfp.pdf">(pdf)</a>
<a href="publications/scfp_appendix.pdf">(appendix)</a>
<a href="publications/scfp_ext.pdf">(pdf+appendix)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. (2015). <b>Structures for structural recursion</b>.
<i>International Conference on Functional Programming, Vancouver, BC, Canada (ICFP2015)</i>.
<br />
<a href="http://dl.acm.org/authorize?N30136">(acm)</a>
<a href="https://doi.org/10.1145/2784731.2784762">(doi)</a>
<a href="publications/structure-recursion.pdf">(pdf)</a>
<a href="publications/structure-recursion-extended.pdf">(extended)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2014). <b>Compositional semantics for composable continuations: from abortive to delimited control</b>.
<i>International Conference on Functional Programming, Gothenburg, Sweden (ICFP2014)</i>.
<br />
<a href="http://dl.acm.org/authorize?N92884">(acm)</a>
<a href="https://doi.org/10.1145/2628136.2628147">(doi)</a>
<a href="publications/compositional-continuations.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen, Luke Maurer, Zena M. Ariola, and Daniele Varacca. (2014). <b>Continuations, processes, and sharing</b>.
<i>Principles and Practice of Declarative Programming, Canterbury, UK (PPDP2014)</i>.
<br />
<a href="http://dl.acm.org/authorize?N30135">(acm)</a>
<a href="https://doi.org/10.1145/2643135.2643155">(doi)</a>
<a href="publications/cpsproc.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2014). <b>The duality of construction</b>.
<i>European Symposium on Programming, Grenoble, France (ESOP2014)</i>.
<br />
<a href="http://dx.doi.org/10.1007/978-3-642-54833-8_14">(doi)</a>
<a href="publications/duality-construction.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin. (2012).
<b>Classical call-by-need sequent calculi: The unity of semantic artifacts</b>.
<i>International Symposium on Functional and Logic Programming, Kobe, Japan (FLOPS2012)</i>.
<br />
<a href="http://dx.doi.org/10.1007/978-3-642-29822-6_6">(doi)</a>
<a href="publications/classical-need-artifacts.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2012). <b>A Systematic Approach to Delimited Control with Multiple Prompts</b>.
<i>European Symposium on Programming, Tallinn, Estonia (ESOP2012)</i>.
<b>Best Paper Award</b> nominee.
<br />
<a href="http://dx.doi.org/10.1007/978-3-642-28869-2_12">(doi)</a>
<a href="publications/systematic-multiple-prompts.pdf">(pdf)</a>
</li>
</ul>
<h3 id="conference-papers">Workshop Abstracts</h3>
<ul>
<li class="fa fa-angle-double-right">
Luke Maurer, Paul Downen, Zena Ariola, and Simon Peyton Jones. (2016). <b>Administrative normal form, continued</b>.
<i>Higher-Order Programming with Effects, Nara, Japan (HOPE2016)</i>.
<br />
<a href="publications/anf-continued.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. (2015). <b>Control controls extensional execution</b>.
<i>Higher-Order Programming with Effects, Vancouver, BC, Canada (HOPE2015)</i>.
<br />
<a href="publications/HOPE2015.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2014). <b>Delimited control with multiple prompts in theory and practice</b>.
<i>Higher-Order Programming with Effects, Gothenburg, Sweden (HOPE2014)</i>.
<br />
<a href="publications/multiple-prompts-tap.pdf">(pdf)</a>
</li>
</ul>
<h3 id="unpublished-manuscripts">Unpublished Manuscripts</h3>
<ul>
<li class="fa fa-angle-double-right">
Paul Downen. (2017). <b>Sequent Calculus: A Logic and a Language for Computation and Duality</b>. Ph.D. thesis, University of Oregon.
<br />
<a href="publications/downen_phd.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen. (2014). <b>Computational Duality and the Sequent Calculus</b>. Comprehensive Area Exam Report, University of Oregon.
<br />
<a href="publications/cdsc.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2021). <b>Classical (Co)Recursion: Programming</b>.
<br />
<a href="https://arxiv.org/abs/2103.06913">(arXiv)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen and Zena M. Ariola. (2017). <b>A Polar Basis for Simple Types</b>.
<br />
<a href="publications/polar-simple-types.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen. (2024). <b>Foundations of Programming Languages</b>. Lecture notes for course at the Oregon Programming Languages Summer School, June 3-8, 2024.
<br />
<a href="notes/oplss24.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen. (2022). <b>Abstract Machines and Classical Realizability</b>. Lecture notes for course at the Oregon Programming Languages Summer School, June 24-27, 2022.
<br />
<a href="notes/amcr.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
Paul Downen. (2014). <b>Bi-orthogonality</b>. Personal notes on bi-orthogonal models of type systems, originally written in August, 2014.
<br />
<a href="notes/biorthogonality_notes.pdf">(pdf)</a>
</li>
</ul>
</article>
<article class="is-post" id="presentations">
<header>
<a href="#"><h2>Presentations</h2></a>
</header>
<h3 id="conference-talks">Conference Talks</h3>
<ul>
<li class="fa fa-angle-double-right">
<b>A Contextual Formalization of Structural Coinduction</b>.
<br /> Venue: International Conference on Functional Programming, Singapore. October 13, 2025.
<br /> Slides: <a href="presentations/cointext-icfp25.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Controlling Copatterns: There and Back Again</b>.
<br /> Venue: OlivierFest, Singapore. October 15, 2025.
<br /> Slides: <a href="presentations/derive-copat-slides.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>CoScheme: Compositional Copatterns in Scheme</b>.
<br /> Venue: Trends in Functional Programming, Oxford, UK. January 16, 2025.
<br /> Slides: <a href="presentations/coscheme-slides.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Call-By-Unboxed-Value</b>.
<br /> Venue: International Conference on Functional Programming, Milan, Italy. September 3, 2024.
<br /> Slides: <a href="presentations/cbuv-slides.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Kinds are Calling Conventions</b>.
<br /> Venue: Programming Language Design and Implementation, San Diego, CA, USA. June 16, 2022.
<br /> Slides: <a href="presentations/kacc-pldi.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>A Computational Understanding of (Co)Recursion</b>.
<br /> Venue: Principles and Practice of Declarative Programming. September 10, 2020.
<br /> Slides: <a href="presentations/ppdp20-slides.pdf">(pdf)</a>
<br /> Video <a href="presentations/ppdp20-talk.mp4">(mp4)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Kinds are Calling Conventions</b>.
<br /> Venue: International Conference on Functional Programming. August 27, 2020.
<br /> Slides: <a href="presentations/kacc-slides.pdf">(pdf)</a>
<br /> Video <a href="presentations/kacc-talk.mp4">(mp4)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Codata in action</b>.
<br /> Venue: European Symposium on Programming, Prague, Czech Republic. April 8, 2019.
<br /> Slides: <a href="presentations/cia.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Beyond Polarity: Towards A Multi-Discipline Intermediate Language with Sharing</b>.
<br /> Venue: Computer Science Logic, Birmingham, UK. September 4, 2019.
<br /> Slides: <a href="presentations/beyond-polarity.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Sequent calculus as a compiler intermediate language</b>.
<br /> Venue: International Conference on Functional Programming, Nara, Japan. September 19, 2016.
<br /> Slides: <a href="presentations/scfp-slides.pdf">(pdf)</a>
<br /> Video: <a href="https://www.youtube.com/watch?v=iF0_NRNIoeY">(youtube)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Structures for structural recursion</b>.
<br /> Venue: International Conference on Functional Programming, Vancouver, BC, Canada. August 31, 2015.
<br /> Slides: <a href="presentations/structure-recursion-slides.pdf">(pdf)</a>
<br /> Video: <a href="https://www.youtube.com/watch?v=rzEFoBNc_ko">(youtube)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Continuations, processes, and sharing</b>.
<br /> Venue: Principles and Practice of Declarative Programming, Canterbury, UK. September 8, 2014.
<br /> Slides: <a href="presentations/cpsproc-slides.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Compositional Semantics for Composable Continuations: From Abortive to Delimited Control</b>.
<br /> Venue: International Conference on Functional Programming, Gothenburg, Sweden. September 1, 2014.
<br /> Slides: <a href="presentations/compositional-continuations-slides.pdf">(pdf)</a>
<br /> Video: <a href="https://www.youtube.com/watch?v=uMQ7Co7OMQU">(youtube)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>The duality of construction</b>.
<br /> Venue: European Symposium on Programming, Grenoble, France. April 9, 2014.
<br /> Slides: <a href="presentations/duality-construction-slides.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>A Systematic Approach to Delimited Control with Multiple Prompts</b>.
<br /> Venue: European Symposium on Programming, Tallinn, Estonia. March 26, 2012.
<br /> Slides: <a href="presentations/systematic-multiple-prompts-slides.pdf">(pdf)</a>
</li>
</ul>
<h3 id="workshop-talks">Workshop Talks</h3>
<ul>
<li class="fa fa-angle-double-right">
<b>Rewriting Macros on the Fly: A Modular Approach to Administrative Reduction During Expansion</b>.
<br /> Venue: Scheme and Functional Programming Workshop, Singapore. October 16, 2025.
<br /> Slides: <a href="presentations/rewrite-macros-slides.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Effective Equality: Overcoming Obstacles with Beta and Eta</b>
<br /> Or: <b>How I Learned to Stop Worrying and Love Control</b>.
<br /> Venue: Shonan 203: Effect Handlers & General Purpose Languages, Shonan Village Center, Japan. September 28, 2023.
<br /> Slides: <a href="presentations/shonan-effeq.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Control as Proof: And the Route to Composition, In Three Parts</b>.
<br /> Venue: Shonan 203: Effect Handlers & General Purpose Languages, Shonan Village Center, Japan. September 28, 2023.
<br /> Slides: <a href="presentations/shonan-controlproof.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Multiple Prompts: in little steps</b>.
<br /> Venue: Shonan 203: Effect Handlers & General Purpose Languages, Shonan Village Center, Japan. September 26, 2023.
<br /> Slides: <a href="presentations/shonan-multiprompt.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Control controls extensional execution</b>.
<br /> Venue: Higher-Order Programming with Effects, Vancouver, BC, Canada. August 30, 2015.
<br /> Slides: <a href="presentations/hope2015-slides.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Delimited control with multiple prompts in theory and practice</b>.
<br /> Venue: Higher-Order Programming with Effects, Gothenburg, Sweden. August 31, 2014.
<br /> Slides: <a href="presentations/multiple-prompts-tap-slides.pdf">(pdf)</a>
<br /> Video: <a href="http://www.youtube.com/watch?v=v5HVEKIQDos&t=30m54s">(youtube)</a>
</li>
</ul>
<h3 id="invited-talks">Invited Talks</h3>
<ul>
<li class="fa fa-angle-double-right">
<b>CoScheme: Compositional Copatterns in Scheme</b>.
<br /> Or: <b>"Equal" Means Equal</b>.
<br /> Venue: Software Seminar, Northeastern University, Boston, MA. January 30, 2026.
<br /> Slides: <a href="presentations/coscheme-northeastern.pdf">(pdf)</a>
<br /> Code: <a href="presentations/coscheme-northeastern-demo.rkt">(rkt)</a>
</li>
<li class="fa fa-angle-double-right">
<b>Contextual Coinduction and Classical Logic</b>
<br /> Or: <b>Fearlessly Observing the Infinite</b>.
<br /> Venue: Principles of Programming and Verification, Boston University, Boston, MA, USA. April 21, 2023.
<br /> Slides: <a href="presentations/coin-popv.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Logic In Action</b>.
<br /> Venue: University of Massachusetts, Lowell, MA. April 15, 2021.
<br /> Venue: University of Vermont, Burlington, VT. March 17, 2021.
<br /> Slides: <a href="presentations/lia.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Kinds Are Calling Convnetions: Intensional Static Polymorphism</b>.
<br /> Venue: Principles of Programming and Verification, Boston University, Boston, MA, USA. November 17, 2020.
<br /> Slides: <a href="presentations/kacc-popv.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Beyond Polarity: Towards A Multi-Discipline Intermediate Language with Sharing</b>.
<br /> Venue: University of Cambridge, UK. September 11, 2019.
<br /> Venue: Microsoft Research, Cambridge, UK. September 10, 2019.
<br /> Slides: <a href="presentations/beyond-polarity.pdf">(pdf)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>The structures of induction and co-induction</b>.
<br /> Venue: Microsoft Research Lecture, Cambridge, UK. September 17, 2015.
</li>
<br />
<li class="fa fa-angle-double-right">
<b>The duality of construction</b>.
<br /> Venue: McGill University, Montreal, QC, Canada. November 6, 2014.
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Building up delimited control with multiple prompts</b>.
<br /> Venue: INRIA Preuves, Programmes et Systèmes, Théorie des types et réalisabilité, Paris, France. December 19, 2012.
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Opening the Black Box: Profiling Computer Memory</b>.
<br /> Venue: Lawrence Technological University, Arts and Science Seminar Series, Southfield, MI, USA. February 11, 2010.
</li>
</ul>
<h3 id="oplss">OPLSS</h3>
<ul>
<li class="fa fa-angle-double-right">
<b>Foundations of Programming Languages</b>
<br /> Venue: Oregon Programming Languages Summer School, Boston University, Boston, MA, USA. June 3–13, 2024.
<br />Site: <a href="https://www.cs.uoregon.edu/research/summerschool/summer24/topics.php#Downen">OPLSS</a>
<br /> Notes: <a href="https://www.cs.uoregon.edu/research/summerschool/summer24/lectures/Downen1.pdf">(pdf)</a>
<br /> Video: <a href="https://youtube.com/playlist?list=PL4TFI2mFNlJCqsi_BV_gv5QEDus78qy7s&si=Nn7sMRc0m9KblOHq">(youtube)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Abstract Machines and Classical Realizability</b>
<br /> Venue: Oregon Programming Languages Summer School, Boston University, Eugene, OR, USA. June 10–July 2, 2022.
<br />Site: <a href="https://www.cs.uoregon.edu/research/summerschool/summer22/topics.php#Downen">OPLSS</a>
<br /> Notes: <a href="https://www.cs.uoregon.edu/research/summerschool/summer22/lectures/Downen_amcr.pdf">(main)</a> <a href="https://www.cs.uoregon.edu/research/summerschool/summer22/lectures/Downen_biorthogonality_notes.pdf">(supplemental)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Foundations of Programming Languages</b>
<br /> Venue: Oregon Programming Languages Summer School, Boston University, Eugene, OR, USA. July 3–8, 2018.
<br />Site: <a href="https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php#review">OPLSS</a>
<br /> Notes: <a href="https://www.cs.uoregon.edu/research/summerschool/summer18/lectures/foundations_notes.pdf">(pdf)</a>
<br /> Video: <a href="https://youtube.com/playlist?list=PL0DsGHMPLUWWQ2kRAeMx-4GkEy4czjigw&si=zVsV36NMC1cDIul_">(youtube)</a>
</li>
<br />
<li class="fa fa-angle-double-right">
<b>Review</b>
<br /> Venue: Oregon Programming Languages Summer School, Boston University, Eugene, OR, USA. July 3–7, 2017.
<br />Site: <a href="https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php#review">OPLSS</a>
</li>
</ul>
</article>
</div>
</div>
</div>
</div>
<!-- Footer Wrapper -->
<div id="footer-wrapper">
<!-- Footer -->
<div id="footer" class="container">
<header id="contact">
<a href="#"><h2>Contact</h2></a>
</header>
<div class="6u">
<section>
<div class="row">
<ul class="icons 8u">
<li class="fa fa-home">
Dandeneau Hall<br />
University of Massachusetts Lowell<br />
Department of Computer Science<br />
1 University Avenue<br />
Lowell, MA 01854
</li>
</ul>
<ul class="icons 2u">
<li class="fa fa-envelope">
<a href="mailto:paul@pauldownen.com">paul@pauldownen.com</a>
</li>
</ul>
</div>
</section>
</div>
</div>
</div>
<!-- Copyright -->
<div id="copyright" class="container">
<ul class="links">
<li></li>© 2021. All rights reserved</li>
<li>Design: <a href="http://html5up.net/">HTML5 UP</a></li>
</ul>
</div>
</div>
</body>
</html>