This repository was archived by the owner on Jul 4, 2021. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 10
Expand file tree
/
Copy pathseminars.html
More file actions
1712 lines (1602 loc) · 209 KB
/
seminars.html
File metadata and controls
1712 lines (1602 loc) · 209 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
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html>
<html lang="en"><head><meta charset="utf-8" />
<meta http-equiv="X-UA-Compatible" content="IE=edge" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<meta property="og:title" content="NEU PRL" />
<meta property="og:description" content="Programming Research Laboratory @ Northeastern&nbsp;University" />
<meta property="og:image" content="img/prl-bg.png" />
<title>Seminars - Programming Research Laboratory - Northeastern University</title>
<!-- Bootstrap -->
<link href="css/bootstrap.min.css" rel="stylesheet" />
<!-- Custom css -->
<link href="css/custom.css" rel="stylesheet" />
<!-- Fonts -->
<link href="https://fonts.googleapis.com/css?family=Ubuntu:300" rel="stylesheet" type="text/css" />
<link href="https://fonts.googleapis.com/css?family=PT+Sans" rel="stylesheet" type="text/css" />
<!-- For IE 9 and below. ICO should be 32x32 pixels in size -->
<!-- [if IE]><link rel="shortcut icon" href="img/favicon.ico"><![endif] -->
<!-- Firefox, Chrome, Safari, IE 11+ and Opera. 196x196 pixels in size. -->
<link rel="icon" href="img/favicon.png" />
<!-- HTML5 shim and Respond.js for IE8 support of HTML5 elements and media queries -->
<!-- WARNING: Respond.js doesn't work if you view the page via file:// -->
<!-- [if lt IE 9] -->
<script src="https://oss.maxcdn.com/html5shiv/3.7.2/html5shiv.min.js"></script>
<script src="https://oss.maxcdn.com/respond/1.4.2/respond.min.js"></script>
<!-- <![endif] --> </head>
<body id="pn-top"><nav class="navbar navbar-inverse"><div class="container"><div class="row"><div class="navbar-header"><button type="button" class="navbar-toggle collapsed" data-toggle="collapse" data-target="#navbar" aria-expanded="false" aria-controls="navbar"><span class="sr-only">Toggle navigation</span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
<span class="icon-bar"></span></button></div>
<div id="navbar" class="navbar-collapse collapse"><ul class="nav navbar-nav"><li role="presentation"><a href="./">Home</a></li><li role="presentation"><a href="people.html">People</a></li><li role="presentation"><a href="teaching.html">Teaching</a></li><li role="presentation" class="active"><a href="#">Seminars</a></li><li role="presentation"><a href="software.html">Software</a></li><li role="presentation"><a href="publications.html">Publications</a></li><li role="presentation"><a href="new-members.html">New Members</a></li><li role="presentation"><a href="contact.html">Contact</a></li><li role="presentation"><a href="blog/index.html">Blog</a></li></ul> </div></div></div></nav>
<div class="jumbotron subpages"><div class="container"><div class="row"><div class="col-md-12"><h1>Seminars</h1></div></div></div></div>
<div class="pn-main-wrapper"><div class="content"><div class="container"> <div class="row"><div class="col-md-12"><h2>Programming Language Seminar</h2>
<p>The PL seminar meets in WVH
[<a href="http://www.ccs.neu.edu/home/wand/directions.html">directions</a>]. The <a href="http://lists.ccs.neu.edu/pipermail/pl-seminar">mailing
list</a> is public. An <a href="https://calendar.google.com/calendar/embed?src=k4cg1vgb3l2n8r2ph4t01dmtpc@group.calendar.google.com&ctz=America/New_York">HTML calendar</a>
and an <a href="https://calendar.google.com/calendar/ical/k4cg1vgb3l2n8r2ph4t01dmtpc%40group.calendar.google.com/public/basic.ics">ICAL calendar</a>
are available for your convenience.</p></div></div>
<br />
<div class="row"><div class="col-md-12"><h3>Upcoming Seminars</h3>
<hr />
<h3>Past Seminars</h3>
<div id="seminar-1" class="col-md-12 pn-seminar finished"><div id="balzer" class="pn-main-informations"><a onclick="return false;" class="pn-title">Manifest Deadlock-Freedom for Shared Session Types</a>
<br />
<span class="pn-name">Stephanie Balzer</span>
<span class="pn-affiliation">Carnegie Mellon University</span>
<a class="pn-url" target="_blank" href="http://www.cs.cmu.edu/~balzers/">http://www.cs.cmu.edu/~balzers/</a>
<br />
<span class="pn-datetime">13 November, 2020 12:00PM <a href="#balzer"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">Video Conference</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed pi-calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to an acquire-release discipline. The resulting language recovers the expressiveness of the untyped asynchronous pi-calculus and accommodates practical programming scenarios, such as shared servers, file systems etc. The resulting language is implemented as a prototype in C0 (a safe subset for C used to teach freshmen at CMU) and <a href="https://github.com/maybevoid/ferrite">as a DSL in Rust</a>.</p>
<p>The generalization, however, comes at the cost of deadlock-freedom, a property which holds for the purely linear fragment. In this talk, I report on recent work that makes up for this deficiency and introduces a type system of linear and shared session types in which the adjoint modalities are complemented with possible worlds to rule out cyclic dependencies between acquires and synchronizations. I distill the key abstractions to reason about cyclic dependencies and the key invariants enforced by the type system to guarantee deadlock-freedom. Time permitted, I report on ongoing work that also uses possible world modalities for type-based verification of program properties of interest.</p>
<p class="pn-title-2">Bio</p>
<p>Stephanie Balzer is a research faculty in the Principles of Programming group in the Computer Science Department at Carnegie Mellon University. Stephanie obtained her PhD from ETH Zurich under the supervision of Thomas R. Gross. In her PhD work, Stephanie developed the sequential relationship-based programming language Rumer and an invariant-based verification technique for Rumer. Stephanie’s current work focuses on the development of type systems and logics for verifying properties of concurrent programs.</p></div></div><br />
<div id="seminar-2" class="col-md-12 pn-seminar finished"><div id="blasband-yafl" class="pn-main-informations"><a onclick="return false;" class="pn-title">Grow your own language: The YAFL story</a>
<br />
<span class="pn-name">Darius Blasband</span>
<span class="pn-affiliation">Raincode</span>
<a class="pn-url" target="_blank" href="https://www.dariusblasband.com">https://www.dariusblasband.com</a>
<br />
<span class="pn-datetime">17 February, 2020 11:00AM <a href="#blasband-yafl"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>This talk tells the rather uncommon story of the co-evolution of my company, Raincode, with a home-grown programming language, YAFL. The two are intimately intertwined: Raincode would crumble if YAFL was to disappear, and YAFL would have no reason to exist if Raincode was to stop its activities. YAFL is a strongly-typed object-oriented language originally designed and implemented a quarter of century ago. Our story starts with YAFL’s inception, its design, our motivations (including the usual fantasies of world domination) and the technical underpinnings and some key implementation decisions.</p>
<p>Our story is rooted in the real-world where pragmatics reign. I will argue that out design choices and implementation decisions have converged to give YAFL its true value, and, that the fruits of growing our own language are well worth the maintenance burden. The talk will argue that YAFL is a non-DSL, and touch on the good ideas as well as the lousy ones. I will discuss how to evolve a language over time by judiciously adding, as well as removing, features. Above all, it is story about people. The language designer, its implementors, its first users, even its customers are the main. Their interplay sheds a light on how languages are created and maintained.</p>
<p class="pn-title-2">Bio</p>
<p>Darius Blasband was born in 1965 and has a PhD from the Université Libre de Bruxelles. His focus is legacy code modernization, articulated around compilers for legacy languages. He founded Raincode (https://www.raincode.com), and designed its core technology. Above all, Darius is a geek. Building software systems is what he likes best—after his family, chocolate, and on par with music.</p></div></div><br />
<div id="seminar-3" class="col-md-12 pn-seminar finished"><div id="mazza-autodiff" class="pn-main-informations"><a onclick="return false;" class="pn-title">Automatic Differentiation in PCF</a>
<br />
<span class="pn-name">Damiano Mazza</span>
<span class="pn-affiliation">CNRS, Université Sorbonne Paris Nord</span>
<a class="pn-url" target="_blank" href="https://lipn.univ-paris13.fr/~mazza/">https://lipn.univ-paris13.fr/~mazza/</a>
<br />
<span class="pn-datetime">28 January, 2020 10:00AM <a href="#mazza-autodiff"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Automatic differentiation (AD) is the science of efficiently computing the derivative (or gradient, or Jacobian) of functions specified by computer programs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for training deep neural networks. Albeit AD techniques natively focus on a restricted class of programs, namely first-order straight-line programs, the rise of so-called differentiable programming in recent years has urged for the need of applying AD to complex programs, endowed with control flow operators and higher-order combinators, such as map and fold. In this talk, I will discuss the extension of AD algorithms to PCF, a(n idealized) purely functional programming language. We will first consider the simply-typed lambda-calculus, showing in particular how linear negation is related to reverse-mode AD (a.k.a., backpropagation), and then see how the extra features of PCF, namely full recursion and conditionals, may be dealt with, stressing the difficulties posed by the latter.</p>
<p>Joint work with Aloïs Brunel (Deepomatic) and Michele Pagani (IRIF, Université de Paris).</p>
<p class="pn-title-2">Bio</p>
<p>Damiano Mazza is chargé de recherche (researcher) at CNRS, working at the CS lab of Université Sorbonne Paris Nord, a position he has held since 2008. He obtained his Ph.D. in 2006 at the Institut de Mathématiques de Luminy, in Marseille. Before that, he studied CS Engineering in Rome, Italy, which is where he is from. His research interest are at the interface between logic in computer science, the theory of programming languages and complexity theory, with a bias towards the viewpoint provided by linear logic and category theory.</p></div></div><br />
<div id="seminar-4" class="col-md-12 pn-seminar finished"><div id="paraskevopoulou-certicoq" class="pn-main-informations"><a onclick="return false;" class="pn-title">CertiCoq: Current and Future Directions</a>
<br />
<span class="pn-name">Zoe Paraskevopoulou</span>
<span class="pn-affiliation">Princeton University</span>
<a class="pn-url" target="_blank" href="http://zoep.github.io">http://zoep.github.io</a>
<br />
<span class="pn-datetime">3 December, 2019 10:00AM <a href="#paraskevopoulou-certicoq"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>In this talk, I will give a high-level overview of CertiCoq, a verified compiler from Coq to C, focusing on my research on CertiCoq's backend. The backend of CertiCoq is based on a micro-pass compiler architecture: each stage in its pipeline performs a simple task, yet they combine to generate efficient code. The micro-pass design along with our proof framework based on logical relations greatly facilities modular reasoning and proof reuse. Furthermore, I will show how this logical relation framework can be extended to provide correctness guarantees for programs compiled separately with CertiCoq, using perhaps different sets of optimizations. Lastly, I will discuss future research directions with CertiCoq, such as provably correct interoperation of Coq and C using the Verified Software Toolchain.</p>
<p class="pn-title-2">Bio</p>
<p>Zoe Paraskevopoulou is a 5th year PhD student at Princeton University, working with professor Andrew Appel. Prior to that she obtained her master's degree from École normale supérieure Paris-Saclay and her undergraduate degree from National Technical University of Athens. She has done several internships at institutes such as INRIA Paris, Max Planck Institute of Software Systems, Microsoft Research and Facebook.</p></div></div><br />
<div id="seminar-5" class="col-md-12 pn-seminar finished"><div id="guha-serverless" class="pn-main-informations"><a onclick="return false;" class="pn-title">Faster, Safer, and Cheaper Serverless Computing using Language-Based Techniques</a>
<br />
<span class="pn-name">Arjun Guha</span>
<span class="pn-affiliation">University of Massachusetts, Amherst</span>
<a class="pn-url" target="_blank" href="https://people.cs.umass.edu/~arjun/main/home/">https://people.cs.umass.edu/~arjun/main/home/</a>
<br />
<span class="pn-datetime">12 November, 2019 10:00AM <a href="#guha-serverless"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Serverless computing is a cloud computing abstraction that makes it easier to write robust, large-scale web services. In serverless computing, programmers write what are called serverless functions, and the cloud platform transparently manages the operating system, resource allocation, load-balancing, and fault tolerance. When demand spikes, the platform automatically allocates additional hardware and manages load-balancing; when demand falls, the platform silently deallocates idle resources; and when the platform detects a failure, it transparently retries affected requests.</p>
<p>In this talk, we will see how language-based techniques can make serverless computing faster, safer, and cheaper for programmers. First, we present a detailed, operational model of a serverless computing platform, which shows that serverless computing is a leaky abstraction. We then derive a less-leaky "naive semantics" and precisely characterize how the two semantics coincide. Second, we extend the operational semantics with a domain-specific language for composing serverless functions, and show that the language design lends itself to an efficient implementation that lowers the cost of building modular applications. Finally, we present a "serverless function accelerator" that significantly reduces the latency of a large class of functions using language-based sandboxing and speculative optimizations.</p>
<p class="pn-title-2">Bio</p>
<p>Arjun Guha is an associate professor of Computer Science at the University of Massachusetts Amherst. Using the tools and techniques of programming languages, his research addresses security, reliability, and performance problems in web applications, systems, networking, and robotics. He received a PhD in Computer Science from Brown University in 2012 and a BA in Computer Science from Grinnell College in 2006.</p></div></div><br />
<div id="seminar-6" class="col-md-12 pn-seminar finished"><div id="jung-rustbelt" class="pn-main-informations"><a onclick="return false;" class="pn-title">Understanding and evolving the Rust programming language</a>
<br />
<span class="pn-name">Ralf Jung</span>
<span class="pn-affiliation">MPI-SWS</span>
<a class="pn-url" target="_blank" href="https://people.mpi-sws.org/~jung/">https://people.mpi-sws.org/~jung/</a>
<br />
<span class="pn-datetime">4 October, 2019 11:00AM <a href="#jung-rustbelt"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Rust is a young and actively developed "systems programming language" that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. This talk is about my research on understanding and evolving this groundbreaking new language.</p>
<p>The first part of the talk is about building formal foundations for the existing Rust language. Rust employs a strong, ownership-based type system to rule out common systems programming anomalies, but then extends the expressive power of this core type system through libraries that internally use unsafe features. Unfortunately, this ``extensible'' aspect of the Rust language makes Rust's safety claims rather non-obvious, and there is good reason to question whether they actually hold. To address this, we have developed RustBelt, the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof supports the extensible nature of Rust's safety story in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe and compositional extension to the language.</p>
<p>The second part is about evolving the semantics of Rust to better support compiler optimizations. In particular, Rust's reference types provide strong aliasing guarantees, which a clever optimizing compiler should be able to exploit. However, if no care is taken, unsafe code (which plays an essential role in the Rust ecosystem, as mentioned above) can subvert these guarantees. To address this, we have developed Stacked Borrows, a new operational semantics for memory accesses in Rust. On the one hand, Stacked Borrows defines an aliasing discipline and declares programs violating it to have undefined behavior, thus making it possible for us to formally verify the soundness of a number of useful type-based intraprocedural optimizations. On the other hand, we have also implemented the Stacked Borrows semantics in Miri, an interpreter for Rust, and run large parts of the Rust standard library test suite in Miri. In so doing, we have validated that our semantics is sufficiently permissive to account for real-world unsafe Rust code.</p>
<p class="pn-title-2">Bio</p>
<p>Ralf Jung is a PhD student at MPI-SWS in Saarbrücken, where he previously completed his undergraduate degree with Saarland University. Ralf’s research interests center around separation logic, operational semantics for low-level languages, (semantic) type systems, and mechanized+modular proof for program verification. Ralf also loves to learn about anything people do with Rust and the ways in which formal methods could help.</p></div></div><br />
<div id="seminar-7" class="col-md-12 pn-seminar finished"><div id="tate-nom" class="pn-main-informations"><a onclick="return false;" class="pn-title">Towards Gradually Typed Nominal Languages</a>
<br />
<span class="pn-name">Ross Tate</span>
<span class="pn-affiliation">Cornell University</span>
<a class="pn-url" target="_blank" href="https://http://www.cs.cornell.edu/~ross/">https://http://www.cs.cornell.edu/~ross/</a>
<br />
<span class="pn-datetime">26 September, 2019 2:00PM <a href="#tate-nom"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Nom demonstrated that efficient and well-behaved gradual typing is possible. But it did so by assuming all code was written using nominal patterns in a simplistic type system. The nominal patterns limit the applicability to existing untyped code, and the simplistic type system limits the applicability to modern industry languages. This talk will present recent results addressing both of these limitations. I will illustrate an implemented design that enables structural patterns to mix with nominal patterns while also providing a variant of the gradual guarantee that ensures interoperability between these patterns and a semantics-preserving migration path from structural patterns into nominal patterns. I will further demonstrate that Nom's design strategy scales to parametric polymorphism, where the key challenge is not actually generic classes or interfaces but rather generic methods and type-argument inference. Although preliminary, experiments suggest that these more expressive designs can still be implemented relatively efficiently, altogether indicating that gradual typing is a viable feature for nominal languages.</p>
<p class="pn-title-2">Bio</p>
<p>Ross Tate is an Assistant Professor in Computer Science at Cornell University and the Director of the Single Open Intermediate Language Initiative. His research combines theoretical foundations with studies of programmer behavior to develop language designs that ascribe to both academic and industrial principles. He collaborates with major programming languages such as Kotlin, WebAssembly, Julia, Ceylon, and Java to inform his work from practice and incorporate his work into practice. Due to his research contributions and industry impact, he was awarded the Dahl Nygaard Junior Prize in 2017.</p></div></div><br />
<div id="seminar-8" class="col-md-12 pn-seminar finished"><div id="gibbons-ans" class="pn-main-informations"><a onclick="return false;" class="pn-title">Asymmetric Numeral Systems</a>
<br />
<span class="pn-name">Jeremy Gibbons</span>
<span class="pn-affiliation">University of Oxford</span>
<a class="pn-url" target="_blank" href="http://www.cs.ox.ac.uk/jeremy.gibbons/">http://www.cs.ox.ac.uk/jeremy.gibbons/</a>
<br />
<span class="pn-datetime">19 June, 2019 10:00AM <a href="#gibbons-ans"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Asymmetric Numeral Systems (ANS) are an entropy-based encoding method introduced by Jarek Duda in 2007, combining the Shannon-optimal compression effectiveness of arithmetic coding with the execution efficiency of Huffman coding. Existing presentations of the ANS encoding and decoding algorithms are somewhat obscured by the lack of suitable presentation techniques; I will present an equational derivation, calculational where it can be, and highlighting the creative leaps where it cannot. This is work to appear at Mathematics of Program Construction in October.</p>
<p class="pn-title-2">Bio</p>
<p>Jeremy Gibbons is Professor of Computing at the University of Oxford, and head of the Algebra of Programming research group there. His research interests are in programming languages, especially functional programming. He is Editor-in-Chief of the Journal of Functional Programming, Past Chair of IFIP WG2.1 on Algorithmic Languages and Calculi, and Past Vice Chair of ACM SIGPLAN.</p></div></div><br />
<div id="seminar-9" class="col-md-12 pn-seminar finished"><div id="maodeferro-pekoe" class="pn-main-informations"><a onclick="return false;" class="pn-title">Safe programming of IoT devices</a>
<br />
<span class="pn-name">Carlos Mão de Ferro</span>
<span class="pn-affiliation">Faculdade de Ciências da Universidade de Lisboa // UMass Boston</span>
<a class="pn-url" target="_blank" href="https://github.com/cajomferro/">https://github.com/cajomferro/</a>
<br />
<span class="pn-datetime">29 May, 2019 10:00AM <a href="#maodeferro-pekoe"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The Internet of Things (IoT) has the potential for being the next industrial revolution, envisioning billions of embedded devices. Because of their limited resources, IoT devices present specific challenges to their programming and deployment. For instance, limited battery lifetime imposes extreme energy-savings efforts, and low RAM and CPU processing power not only restrict computation power but can also lead to unexpected runtime errors (e.g, out of memory).</p><p>C and C++ languages are often preferred when programming these devices. These languages deliver good performance but are notoriously unsafe and ill-suitable for proving high-level properties specific to HW usage (e.g., sending a message only when Wi-Fi module is connected). Invalid program behaviors can lead to silent errors and energy wasting, resulting in the high-cost of reprogramming thousands of devices.</p><p>In this presentation, I will introduce Pekoe, a language for programming IoT devices that can determine, at compile time, the correct usage of hardware components. Pekoe introduces Harel Statecharts as types to model the hardware behavior. The compiler checks every possible execution trace of a program against the hardware model (the type) thus ensuring the correct order of system calls (e.g., sending a message via Wi-Fi, or suspending the CPU).</p>
<p class="pn-title-2">Bio</p>
<p>Carlos Mão de Ferro is a visiting Fulbright scholar at UMass Boston (February to July 2019), and is a PhD candidate in Computer Science, University of Lisbon, Portugal.</p><p>His research focuses on new programming languages techniques that deliver a safe and resource-aware programming of embedded devices, thus promoting a reliable and sustainable Internet of Things (IoT) environment.</p><p>Carlos has been working on WSNs and embedded software for 10 years. After his master thesis conclusion in 2013, he alternated between the academia and the industry worlds. Carlos developed a smart irrigation system for the Green by Web startup that won the Smart Open Lisboa Startup contest in 2017.</p><p>In general, Carlos is curious about Science and driven by the desire to understand how things work and how discoveries and inventions come to see the light of day. He enjoys reading topics about Physics, Astronomy and Biology. He is also passionate about music, having learned to play the flute and the piano as a child.</p><p>During his stay at UMB, Carlos will be particularly interested in foster collaborations with researchers from IoT-related areas.</p></div></div><br />
<div id="seminar-10" class="col-md-12 pn-seminar finished"><div id="pfenning-message-passing-concurrency" class="pn-main-informations"><a onclick="return false;" class="pn-title">A rehabilitation of message-passing concurrency</a>
<br />
<span class="pn-name">Frank Pfenning</span>
<span class="pn-affiliation">Carnegie Mellon University</span>
<a class="pn-url" target="_blank" href="http://www.cs.cmu.edu/~fp/index.html">http://www.cs.cmu.edu/~fp/index.html</a>
<br />
<span class="pn-datetime">2 May, 2019 10:00AM <a href="#pfenning-message-passing-concurrency"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Recently, there has been a lot of research on shared-memory concurrency. Nevertheless, programmers are discouraged from using it because of the difficulty of writing clear, correct programs. This is embodied for example in the Go Language slogan “Do not communicate by sharing memory; instead, share memory by communicating.” But do we have the right abstractions for message-passing concurrent programming? I argue that we do not (yet!) because concurrency constructs are usually bolted on to an existing language with an entirely different semantic foundation. I will review some recent progress on designing better abstractions based on strong logical and type-theoretic principles. Multiple themes from functional and object-oriented programming will re-emerge from these foundations in a new form, including (ha!) shared memory.</p>
<p class="pn-title-2">Bio</p>
<p>Frank Pfenning studied Mathematics and Computer Science at the Technical University Darmstadt and then left for Carnegie Mellon University on a Fulbright scholarship where he obtained his Ph.D. in Mathematics in 1987 under the supervision of Professor Peter Andrews. He subsequently joined the Department of Computer Science at Carnegie Mellon University as research faculty where he became Professor in 2002 and served as Director of Graduate Programs from 2004 to 2008 and Associate Dean for Graduate Education from 2009 to 2010. He was the Joseph F. Traub Professor of Computer Science and Head of the Computer Science Department from 2013 to 2018. He has spent time as visiting scientist at the Max-Planck-Institute for Computer Science in Saarbrücken, as Alexander-von-Humboldt fellow at the Technical University Darmstadt, and as visiting professor at École Polytechnique and INRIA-Futurs. He has advised 24 completed Ph.D. theses and won the Herbert A. Simon Award for Teaching Excellence in the School of Computer Science in 2002. He served as trustee, vice president, and president of CADE, Inc., the governing body of the International Conference on Automated Deduction, and on advisory boards for INRIA, the Max-Planck-Institute for Computer Science, and Seoul National University. He has chaired several conferences and program committees, including CADE and LICS, and has been a member of the editorial boards for Theoretical Computer Science, Journal of Automated Reasoning, and the Journal of Symbolic Computation. He was named Fellow of the ACM in 2015. His research interests include programming languages, logic and type theory, logical frameworks, automated deduction, and computer security. In his spare time he enjoys playing squash, running, hiking, cooking, and reading.</p></div></div><br />
<div id="seminar-11" class="col-md-12 pn-seminar finished"><div id="bornholt-optimizing-the-automated-programming-stack" class="pn-main-informations"><a onclick="return false;" class="pn-title">Optimizing the Automated Programming Stack</a>
<br />
<span class="pn-name">James Bornholt</span>
<span class="pn-affiliation">University of Washington</span>
<a class="pn-url" target="_blank" href="https://homes.cs.washington.edu/~bornholt/">https://homes.cs.washington.edu/~bornholt/</a>
<br />
<span class="pn-datetime">27 March, 2019 10:00AM <a href="#bornholt-optimizing-the-automated-programming-stack"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The scale and pervasiveness of modern software poses a challenge for programmers: software reliability is more important than ever, but the complexity of computer systems continues to grow. Automated programming tools are powerful weapons for programmers to tackle this challenge: verifiers that check software correctness, and synthesizers that generate new correct-by-construction programs. These tools are most effective when they apply domain-specific optimizations, but doing so today requires considerable formal methods expertise. In this talk, I present a new application-driven approach to optimizing the automated programming stack underpinning modern domain-specific tools. I will demonstrate the importance of programming tools in the context of memory consistency models, which define the behavior of multiprocessor CPUs and whose subtleties often elude even experts. Our new tool, MemSynth, automatically synthesizes formal descriptions of memory consistency models from examples of CPU behavior. We have used MemSynth to synthesize descriptions of the x86 and PowerPC memory models, each of which previously required person-years of effort to describe by hand, and found several ambiguities and underspecifications in both architectures. I will then present symbolic profiling, a new technique we designed and implemented to help people identify the scalability bottlenecks in automated programming tools. These tools use symbolic evaluation, which evaluates all paths through a program, and is an execution model that defies both human intuition and standard profiling techniques. Symbolic profiling diagnoses scalability bottlenecks using a novel performance model for symbolic evaluation that accounts for all-paths execution. We have used symbolic profiling to find and fix performance issues in 8 state-of-the-art automated tools, improving their scalability by orders of magnitude, and our techniques have been adopted in industry. Finally, I will give a sense of the importance of future application-driven optimizations to the automated programming stack, with applications that inspire improvements to the stack and in turn beget even more powerful automated tools.</p>
<p class="pn-title-2">Bio</p>
<p>James Bornholt is a Ph.D. candidate in the Paul G. Allen School of Computer Science & Engineering at the University of Washington, advised by Emina Torlak, Dan Grossman, and Luis Ceze. His research interests are in programming languages and formal methods, with a focus on automated program verification and synthesis. His work has received an ACM SIGPLAN Research Highlight, two IEEE Micro Top Picks selections, an OSDI best paper award, and a Facebook Ph.D. fellowship.</p></div></div><br />
<div id="seminar-12" class="col-md-12 pn-seminar finished"><div id="hobor-mechanized-verification-of-graph-manipulating-programs" class="pn-main-informations"><a onclick="return false;" class="pn-title">Mechanized Verification of Graph-manipulating Programs</a>
<br />
<span class="pn-name">Aquinas Hobor</span>
<span class="pn-affiliation">Yale-NUS College and the School of Computing, National University of Singapore</span>
<a class="pn-url" target="_blank" href="https://www.comp.nus.edu.sg/~hobor/">https://www.comp.nus.edu.sg/~hobor/</a>
<br />
<span class="pn-datetime">22 March, 2019 10:00AM <a href="#hobor-mechanized-verification-of-graph-manipulating-programs"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Graph-manipulating programs such as garbage collectors are notoriously unpleasant to reason about, which is unfortunate since such programs are also used in critical algorithms and systems. We show how to verify such programs written in real C in a fully machine-checked context.</p>
<p class="pn-title-2">Bio</p>
<p>Aquinas Hobor is an Assistant Professor with a joint appointment at Yale-NUS College and the School of Computing, National University of Singapore. From 2008-2011 he was a Lee Kuan Yew Postdoctoral Fellow after getting his PhD from Princeton University. He grew up near Chicago and his Go ranking is approximately 1-dan.</p></div></div><br />
<div id="seminar-13" class="col-md-12 pn-seminar finished"><div id="francois-from-c-to-java-ee-to-node-js" class="pn-main-informations"><a onclick="return false;" class="pn-title">From C to Java EE to Node.js: A Journey in Industrial Program Analysis</a>
<br />
<span class="pn-name">François Gauthier</span>
<span class="pn-affiliation">Oracle Labs Australia</span>
<a class="pn-url" target="_blank" href="https://labs.oracle.com/pls/apex/f?p=labs:bio:0:2080">https://labs.oracle.com/pls/apex/f?p=labs:bio:0:2080</a>
<br />
<span class="pn-datetime">19 March, 2019 10:00AM <a href="#francois-from-c-to-java-ee-to-node-js"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 462</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>I will divide my presentation in two short talks. In the first part of my presentation, I will describe how static analysis of C/C++, our lab's initial expertise, widely differs from static analysis of Java EE, and describe some of the challenges we encountered in the Wafer project. In the second part of my talk, I will describe how we scale dynamic security analysis for Node.js with taint inference, and how the Affogato project compares to state-of-the-art.</p>
<p class="pn-title-2">Bio</p>
<p>François Gauthier graduated in 2014 from Polytechnique Montreal with a PhD in Software Engineering. The same year, he joined the program analysis team at Oracle Labs Australia, under the direction of Dr. Cristina Cifuentes, to start and lead the Wafer project for static vulnerability detection in Java EE. In June 2017, he transitioned to, and is now leading the Affogato project for dynamic security analysis of Node.js. Apart from application security, François is also exploring program analysis and machine learning approaches to detect document-based malware as well as fuzzing techniques to automatically generate test inputs.</p></div></div><br />
<div id="seminar-14" class="col-md-12 pn-seminar finished"><div id="pichardie-verification-of-constant-time-implementations-in-a-verified-compiler-toolchain" class="pn-main-informations"><a onclick="return false;" class="pn-title">Verification of constant-time implementations in a verified compiler toolchain</a>
<br />
<span class="pn-name">David Pichardie</span>
<span class="pn-affiliation">ENS Rennes</span>
<a class="pn-url" target="_blank" href="https://people.irisa.fr/David.Pichardie/">https://people.irisa.fr/David.Pichardie/</a>
<br />
<span class="pn-datetime">6 March, 2019 10:00AM <a href="#pichardie-verification-of-constant-time-implementations-in-a-verified-compiler-toolchain"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Constant-time programming is an established discipline to secure programs against timing attackers. Several real-world secure C libraries such as NaCl, mbedTLS, or Open Quantum Safe, follow this discipline. We propose two advanced compile-time verification techniques to enforce this discipline. The first one operates at assembly level with help from alias informations that are computed at source level and transmitted by the compiler. The second one operates at source level, using advanced abstract interpretation techniques. For this last approach, we also study how to ensure that the compiler will not break the property during compilation. These techniques have been implemented in the CompCert compiler toolchain and tested on several crypto libraries. These works have been presented at CCS’14, CSF’17 and ESORICS’17.</p>
<p class="pn-title-2">Bio</p>
<p>I am professor of Computer Science and head of the Department of Computer Science at ENS Rennes. My research activities take place in the Celtique team (joint team between University of Rennes, ENS Rennesand Inria Rennes, under the IRISA joint lab). I received a Ph.D. in Computer Science from the University of Rennes, France, in 2005, and a Habilitation à diriger les recherches in Computer Science from the ENS Cachan, France, in 2012. I joined ENS Cachan in September 2013 as full professor (in 2014, the brittany extension of ENS Cachan has becomed ENS Rennes). Between 2007 and 2013, I was a full research at INRIA Rennes research center. Earlier, I was holding a postdoc position at INRIA Sophia-Antipolis under the supervision of Gilles Barthe. In the 2011-13 academic years, I took a sabbatical and visited Jan Vitek's group at Purdue University, Indiana, USA, during the first year, and then Greg Morrisett's group at Harvard University, Cambridge, USA, during the second year. My research interests include formal methods, programming languages, program verification, software, and system security. I am a long time happy user of the Coq proof assistant and the theory of Abstract interpretation. More recently I have been conducting several researches about the verified C compiler CompCert. My research is currently funded by an ERC Consolidator Grant "VESTA: VErified STatic Analysis platform" (2018-2023).</p></div></div><br />
<div id="seminar-15" class="col-md-12 pn-seminar finished"><div id="thakur-compare-less-defer-more" class="pn-main-informations"><a onclick="return false;" class="pn-title">Compare Less, Defer More: Scaling Value-Contexts Based Whole-Program Heap Analyses</a>
<br />
<span class="pn-name">Manas Thakur</span>
<span class="pn-affiliation">PACE Lab, Indian Institute of Technology Madras</span>
<a class="pn-url" target="_blank" href="http://www.cse.iitm.ac.in/~manas/">http://www.cse.iitm.ac.in/~manas/</a>
<br />
<span class="pn-datetime">21 February, 2019 10:00AM <a href="#thakur-compare-less-defer-more"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">Ryder 431</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The precision of heap analyses determines the precision of several associated optimizations, and has been a prominent area in compiler research. It has been shown that context-sensitive heap analyses are more precise than the insensitive ones, but their scalability continues to be a cause of concern. Though the value-contexts approach improves the scalability of classical call-string based context-sensitive analyses, it still does not scale well for several popular whole-program heap analyses. In this talk, I will discuss our three-staged approach that lets us scale complex whole-program value-contexts based heap analyses for large programs. The ideas involved are based on an important observation that we do not need to compare the complete value-contexts at each call-site. Apart from this, I will also give an overview of another work, named PYE (for "precise-yet-efficient”). PYE helps obtain precise results during just-in-time compilation efficiently, by splitting the work between the static Java compiler and the C2 compiler of the HotSpot JVM.</p>
<p class="pn-title-2">Bio</p>
<p>Manas is a PhD student under V. Krishna Nandivada at PACE Lab, IIT Madras. His current research focuses on balancing the precision-scalability tradeoffs while analyzing programs written in object-oriented languages. He has worked with the Soot optimization framework for static analyses, and the HotSpot JVM for just-in-time analyses. Apart from work, he writes articles on GitHub and Medium (technical and otherwise!), and experiments with Vim plugins when feeling geeky.</p></div></div><br />
<div id="seminar-16" class="col-md-12 pn-seminar finished"><div id="hur-promising-arm-risc-v-a-simpler-and-faster-operational-concurrency-model" class="pn-main-informations"><a onclick="return false;" class="pn-title">Promising-ARM/RISC-V: a simpler and faster operational concurrency model</a>
<br />
<span class="pn-name">Chung-Kil Hur</span>
<span class="pn-affiliation">Software Foundations Lab, Seoul National University</span>
<a class="pn-url" target="_blank" href="https://sf.snu.ac.kr/gil.hur/">https://sf.snu.ac.kr/gil.hur/</a>
<br />
<span class="pn-datetime">15 February, 2019 10:00AM <a href="#hur-promising-arm-risc-v-a-simpler-and-faster-operational-concurrency-model"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">Ryder 431</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>For ARMv8 and RISC-V, there are concurrency models in two styles, extensionally equivalent: axiomatic models, expressing the concurrency semantics in terms of global properties of complete executions; and operational models, that compute incrementally. The latter are in an abstract micro-architectural style: they execute each instruction in multiple steps, out-of-order and with explicit branch speculation. This similarity to hardware implementations has been important in developing the models and in establishing confidence, but involves complexity that, for programming and model-checking, one would prefer to avoid. In this talk, I will present new more abstract operational models for ARMv8 and RISC-V, and an exploration tool based on them. The models compute the allowed concurrency behaviours incrementally based on thread-local conditions and are significantly simpler than the existing operational models: executing instructions in a single step and (with the exception of early writes) in program order, and without branch speculation. We prove the models equivalent to the existing ARMv8 and RISC-V axiomatic models in Coq. The exploration tool is the first such tool for ARMv8 and RISC-V fast enough for exhaustively checking the concurrency behaviour of a number of interesting examples. We demonstrate using the tool for checking several standard concurrent datastructure and lock implementations such as Michael-Scott queue and Chase-Lev deque, compiled from C++ and Rust with GCC or Clang -O3, and for interactively stepping through model-allowed executions for debugging.</p>
<p class="pn-title-2">Bio</p>
<p>Chung-Kil Hur is an associate professor in Department of Computer Science and Engineering at Seoul National University. Previously he worked as a postdoctoral researcher at Microsoft Research Cambridge,Max Planck Institute for Software Systems (MPI-SWS) and Laboratoire PPS. He obtained a Ph.D. from University of Cambridge and a B.Sc. in both Computer Science and Mathematics from Korea Advanced Institute of Science and Technology (KAIST). His current research interests are in semantics of low-level languages such as C,Rust,LLVM IR, relaxed memory concurrency, formal verification of software such as compiler and OS, and interactive theorem provers such as Coq.</p></div></div><br />
<div id="seminar-17" class="col-md-12 pn-seminar finished"><div id="gonzalez-path-based-function-embedding-and-its-application-to-error-handling-specification-mining" class="pn-main-informations"><a onclick="return false;" class="pn-title">Path-Based Function Embedding and Its Application to Error-Handling Specification Mining</a>
<br />
<span class="pn-name">Cindy Rubio González</span>
<span class="pn-affiliation">University of California, Davis</span>
<a class="pn-url" target="_blank" href="http://web.cs.ucdavis.edu/~rubio/">http://web.cs.ucdavis.edu/~rubio/</a>
<br />
<span class="pn-datetime">14 February, 2019 10:00AM <a href="#gonzalez-path-based-function-embedding-and-its-application-to-error-handling-specification-mining"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">Ryder 431</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Identifying relationships among program elements is useful for program understanding, debugging, and analysis. One such kind of relationship is synonymy. Function synonyms are functions that play a similar role in code; examples include functions that perform initialization for different device drivers, and functions that implement different symmetric-key encryption schemes. Function synonyms are not necessarily semantically equivalent and can be syntactically dissimilar; consequently, approaches for identifying code clones or functional equivalence cannot be used to identify them. In this talk I will present our recent work Func2vec, a technique that learns an embedding that maps each function to a vector in a continuous vector space such that vectors for function synonyms are in close proximity. We compute the function embedding by training a neural network on sentences generated using random walks over the interprocedural control-flow graph. We show the effectiveness of Func2vec at identifying function synonyms in the Linux kernel, and its applicability to the problem of mining error-handling specifications in Linux file systems and drivers.</p>
<p class="pn-title-2">Bio</p>
<p>Cindy Rubio-Gonzalez is an Assistant Professor of Computer Science at the University of California, Davis. Prior to that position, she was a Postdoctoral Researcher in the EECS Department at the University of California, Berkeley. She received her Ph.D. in Computer Science from the University of Wisconsin--Madison in 2012. Cindy's work spans the areas of Programming Languages and Software Engineering, with a focus on program analysis for automated bug finding, program optimization,and software reproducibility. She is particularly interested in the reliability and performance of systems software and scientific computing applications. She currently leads the BugSwarm project,which collects and automatically reproduces thousands of real-world bugs from public software repositories. Among other awards, Cindy is a recipient of an NSF CAREER award 2018, Hellman Fellowship 2017, and UC Davis CAMPOS Faculty Award 2014.</p></div></div><br />
<div id="seminar-18" class="col-md-12 pn-seminar finished"><div id="titzer-what-spectre-means-for-language-implementor" class="pn-main-informations"><a onclick="return false;" class="pn-title">What Spectre means for language implementors</a>
<br />
<span class="pn-name">Ben L. Titzer</span>
<span class="pn-affiliation">Google</span>
<a class="pn-url" target="_blank" href="http://research.google.com/pubs/BenTitzer.html">http://research.google.com/pubs/BenTitzer.html</a>
<br />
<span class="pn-datetime">13 February, 2019 10:00AM <a href="#titzer-what-spectre-means-for-language-implementor"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">Ryder 155</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Until now, CPU designers and computer scientists have assumed Vegas rules at the hardware level: what happens in speculation stays in speculation. Yet in the wake of the Spectre and Meltdown attacks, it has become clear a new, massive class of security vulnerabilities awaits us at the microarchitectural level because this assumption is simply false. As language designers and implementors familiar with building towers of abstractions, we have assumed that virtualization through emulation made the worlds below the Turing machine undetectable, hidden behind a mathematically perfect mirror. This talk will explore how we have now learned to see through that mirror, into the very bizarre and alien world of microarchitectures, illuminating a tiny world of astounding complexity that holds profound implications for language security.</p>
<p class="pn-title-2">Bio</p>
<p>Ben L. Titzer leads Google's WebAssembly team in Munich. Before starting the WebAssembly project with Luke Wagner from Mozilla, he led the team that built the TurboFan optimizing compiler which now powers JavaScript and WebAssembly in V8. He graduated with a BS from Purdue University in 2002 and MS and PhD from UCLA in 2004 and 2007. His interests include safe programming languages for systems programming, compilers, virtual machines, nature and playing guitar.</p></div></div><br />
<div id="seminar-19" class="col-md-12 pn-seminar finished"><div id="waye-whip-contract-service" class="pn-main-informations"><a onclick="return false;" class="pn-title">Whip: Higher-order Contracts for Modern Services</a>
<br />
<span class="pn-name">Lucas Waye</span>
<span class="pn-affiliation">Facebook</span>
<a class="pn-url" target="_blank" href="http://lucaswaye.com/">http://lucaswaye.com/</a>
<br />
<span class="pn-datetime">6 February, 2019 10:00AM <a href="#waye-whip-contract-service"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Modern service-oriented applications forgo semantically rich protocols and middleware when composing services. Instead, they embrace the loosely-coupled development and deployment of services that communicate via simple network protocols. Even though these applications do expose interfaces that are higher-order in spirit, the simplicity of the network protocols forces them to rely on brittle low-level encodings. To bridge the apparent semantic gap, programmers introduce ad-hoc and error-prone defensive code. Inspired by Design by Contract, we choose a different route to bridge this gap. We introduce Whip, a contract system for modern services. Whip (i) provides programmers with a higher-order contract language tailored to the needs of modern services; and (ii) monitors services at run time to detect services that do not live up to their advertised interfaces. Contract monitoring is local to a service. Services are treated as black boxes, allowing heterogeneous implementation languages without modification to services' code. Thus, Whip does not disturb the loosely coupled nature of modern services.</p>
<p class="pn-title-2">Bio</p>
<p>I'm currently a Software Engineer at Facebook thinking about privacy in the data warehouse. Previously I helped build TiVo's Targeted Audience Delivery platform. And before that I worked on the backend for Timeful (acquired by Google) and on Hulu's analytics platform. In graduate school I worked on Whip, a contract monitor for microservices. I received a Ph.D. and Master's degree from Harvard under the guidance of Stephen Chong and a Bachelor's degree from Cornell.</p></div></div><br />
<div id="seminar-20" class="col-md-12 pn-seminar finished"><div id="fare-better-stories-reframing-from-programs-to-programming" class="pn-main-informations"><a onclick="return false;" class="pn-title">Better Stories, Better Languages — Reframing from Programs to Programming</a>
<br />
<span class="pn-name">François-René Rideau</span>
<span class="pn-affiliation">Alacris</span>
<a class="pn-url" target="_blank" href="http://fare.tunes.org">http://fare.tunes.org</a>
<br />
<span class="pn-datetime">30 January, 2019 10:00AM <a href="#fare-better-stories-reframing-from-programs-to-programming"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Software tools imply a story. New stories can help invent new tools. Explicit stories are a great meta-tool... and provide a systematic way to improve the design of programming language design. To illustrate my point, I will present a series of pairs of stories, each time approaching a same topic with very different consequences. Many of my stories will be familiar to most of you, some other stories less so. Hopefully they will be enlightening as well as entertaining... and so will the meta-story be. (Earlier versions of this talk were given at International Lisp Conference 2009, Lisp NYC 2014-10, and more recently LambdaConf 2017.)</p>
<p class="pn-title-2">Bio</p>
<p>François-René Rideau is Co-Founder and Chief Architect at Alacris.io,a company developing a "Blockchain Layer 2 Operating System" using formal methods. Once founder of the TUNES Project, he left academic research on Programming Languages and Distributed Systems to build industrial software at ITA Software, then Google and Bridgewater Associates, before he finally became his own Entrepreneur. Long-standing member of the Lisp community, he runs the Boston Lisp Meeting and still co-maintains ASDF (the Common Lisp build system),though he recently jumped ship to Gerbil Scheme, and now uses OCaml at work.</p></div></div><br />
<div id="seminar-21" class="col-md-12 pn-seminar finished"><div id="chris-goblins-and-spritely" class="pn-main-informations"><a onclick="return false;" class="pn-title">Goblins and Spritely: from the actor model to distributed virtual worlds</a>
<br />
<span class="pn-name">Christoper Lemmer Webber</span>
<span class="pn-affiliation">ActivityPub</span>
<a class="pn-url" target="_blank" href="https://dustycloud.org/">https://dustycloud.org/</a>
<br />
<span class="pn-datetime">5 December, 2018 10:00AM <a href="#chris-goblins-and-spritely"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room">| <a class="pn-url" target="_blank" href="https://github.com/nuprl/website/blob/master/seminar-notes/chris-goblins-and-spritely.txt">Notes</a></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Goblins is an actor model implementation for Racket, inspired by object-capability secure distributed progamming languages such as E with a few new twists of its own thrown in. Goblins is the foundation for a project to build secure, player/user-programmable virtual worlds named Spritely. Spritely builds on the success of the ideas from the ActivityPub protocol, which has succeeded at connecting together various distributed social network projects, extending them to pull in rich interactive and game aspects. See what is built so far, what's coming next, and how the actor model and object capabilities tie together all these ideas to enable a robust and secure distributed system.</p>
<p class="pn-title-2">Bio</p>
<p>Christopher Lemmer Webber is a user freedom advocate who works on distributed social network technology. They are most well known for their work on the W3C ActivityPub federated protocol, which connects over 1.5 million users across the distributed social web. Chris enjoys programming in lisp/scheme flavored languages, especially Racket.</p></div></div><br />
<div id="seminar-22" class="col-md-12 pn-seminar finished"><div id="vitaly-language-development-standardization-haskell" class="pn-main-informations"><a onclick="return false;" class="pn-title">Programming language development and standardization: How they (don’t) do in Haskell</a>
<br />
<span class="pn-name">Vitaly Bragilevsky</span>
<span class="pn-affiliation">Southern Federal University</span>
<a class="pn-url" target="_blank" href="http://sfedu.ru/www/stat_pages22.show?p=RR/per_eng/D&params=(p_per_id=%3E2733)">http://sfedu.ru/www/stat_pages22.show?p=RR/per_eng/D&params=(p_per_id=%3E2733)</a>
<br />
<span class="pn-datetime">28 November, 2018 10:00AM <a href="#vitaly-language-development-standardization-haskell"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Programming languages differ a lot in the ways of their development. Who is responsible for including new features and removing obsolete ones? What is a process of doing that? Is there any more or less formal language definition? How respected is that definition by the compilers? How is this changed if there is only one compiler? These questions are answered quite differently for various programming languages. Haskell takes its own way which was crystallized relatively recently. We have GHC Proposals in the form of the GitHub pull requests to suggest new language features. We also have the GHC Steering Committee with its own process to either accept or reject proposals. Finally, there is the Haskell 2020 Language (Haskell Prime) Committee with its own problem of being effectively dead. In this talk, I’d like to describe how this system works for Haskell and why it doesn’t work sometimes. I will discuss the most recent examples of transforming Haskell kinds system towards dependent types (started before the GHC Steering Committee was formed) and introducing linear types in Haskell (subject to the full-blown Committee discussion) among others. I will also characterize the current state and perspectives of the Haskell standardization process.</p>
<p class="pn-title-2">Bio</p>
<p>Vitaly Bragilevsky serves as both the Haskell 2020 Language Committee and the GHC Steering Committee member. He works as a Senior Lecturer at the Southern Federal University in Rostov-on-Don, Russia where he teaches undergraduate students functional programming and theory of computations. He is currently a grantee of the Fulbright Faculty Development Program holding temporary Courtesy Research Assistant position at the University of Oregon under the supervision of Prof. Zena Ariola. Vitaly Bragilevsky translated into Russian and edited translations of the several books on Haskell and the theory of programming languages. He is the author of ‘Haskell in Depth’ (Manning Publications, available via Manning’s early access program).</p></div></div><br />
<div id="seminar-23" class="col-md-12 pn-seminar finished"><div id="heineman-synthesize-expression-problem" class="pn-main-informations"><a onclick="return false;" class="pn-title">Synthesizing Solutions to the Expression Problem</a>
<br />
<span class="pn-name">George T. Heineman</span>
<span class="pn-affiliation">Worcester Polytechnic Institute</span>
<a class="pn-url" target="_blank" href="https://www.wpi.edu/people/faculty/heineman">https://www.wpi.edu/people/faculty/heineman</a>
<br />
<span class="pn-datetime">17 October, 2018 10:00AM <a href="#heineman-synthesize-expression-problem"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The Expression Problem (EP) describes a common software issue that appears regardless of programming language or programming paradigm. As coined by Philip Wadler in 1998, EP is a new name for an old problem. Given a data type defined by cases, consider two independent extensions, namely, adding new cases to the data type and new functions over the datatype. Dozens of papers in the research literature present their solutions to the EP, using a variety of programming languages and approaches. In this talk I present a Scala-based framework that can synthesize full solutions to the EP problem. The first step is to model the domain of interest (such as mathematical expressions or geometric shapes) to ensure that our synthesized code can work with any desired application domain. Second, we demonstrate how to synthesize code that reproduces a dozen EP solutions from the literature, in C++, Java and Haskell. We designed a common API for all approaches, independent of programming language. While we do not introduce any new approach for EP, we explore the challenges that EP solutions face with binary methods and producer methods. An important contribution of this work is the scientific reproduction of known solutions from the literature.
This work is based on an ongoing collaboration with with Jan Bessai (TU Dortmund) and Boris Düdder (Univ. Copenhagen).</p>
<p class="pn-title-2">Bio</p>
<p>George T. Heineman is an Associate Professor of Computer Science at WPI. His research interests are in Software Engineering, specifically synthesizing software systems from composable units. He is co-author of "Algorithms in a Nutshell (2ed)," published by O'Reilly Media in 2016. Aside from his professional pursuits, George is an avid puzzler. He invented Sujiken(R), a Sudoku variation played on a right-triangle arrangement of cells in which numbers cannot repeat in a horizontal row, vertical column or diagonal in any direction.</p></div></div><br />
<div id="seminar-24" class="col-md-12 pn-seminar finished"><div id="greenberg-posix-shell" class="pn-main-informations"><a onclick="return false;" class="pn-title">Rehabilitating the POSIX shell</a>
<br />
<span class="pn-name">Michael Greenberg</span>
<span class="pn-affiliation">Pomona College</span>
<a class="pn-url" target="_blank" href="http://www.cs.pomona.edu/~michael/">http://www.cs.pomona.edu/~michael/</a>
<br />
<span class="pn-datetime">10 October, 2018 10:00AM <a href="#greenberg-posix-shell"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>We build intricate systems with complex algorithms and invariants, aiming for guarantees of correctness and performance... and then we maintain and deploy these systems with shell scripts! What *are* shell scripts? If the POSIX shell is a programming language, what are its syntax and semantics? Can we apply PL tools to reason about the shell? Why haven't prior PL attempts at understanding the shell redeemed it?</p>
<p class="pn-title-2">Bio</p>
<p>Michael Greenberg is an assistant professor at Pomona College. He received his BA in Computer Science and Egyptology from Brown University (2007) and his PhD in Computer Science from the University of Pennsylvania (2013). His work has ranged from functional-reactive JavaScript (with Shriram Krishnamurthi at Brown) to runtime verification of higher-order programs using contracts (with Benjamin Pierce at Penn) to software-defined networking (with Dave Walker at Princeton) to present activities focused on Kleene algebra with tests and the POSIX shell. He is always looking for new climbing partners.</p></div></div><br />
<div id="seminar-25" class="col-md-12 pn-seminar finished"><div id="cifuentes-parfait-vulnerability-detection" class="pn-main-informations"><a onclick="return false;" class="pn-title">Oracle Parfait: The Flavour of Real-World Vulnerability Detection</a>
<br />
<span class="pn-name">Cristina Cifuentes</span>
<span class="pn-affiliation">Oracle Labs</span>
<a class="pn-url" target="_blank" href="https://labs.oracle.com/pls/apex/f?p=labs:bio:0:21">https://labs.oracle.com/pls/apex/f?p=labs:bio:0:21</a>
<br />
<span class="pn-datetime">3 October, 2018 1:15PM <a href="#cifuentes-parfait-vulnerability-detection"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVF 010</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The Parfait static code analysis tool focuses on detecting vulnerabilities that matter in C, C++, Java and PL/SQL languages. Its focus has been on key items expected out of a commercial tool that lives in a commercial organization, namely, precision of results (i.e., high true positive rate), scalability (i.e., being able to run quickly over millions of lines of code), incremental analysis (i.e., being able to run over deltas of the code quickly), and usability (i.e., ease of integration into standard build processes, reporting of traces to the vulnerable location, etc). Today, Parfait is used by thousands of developers at Oracle worldwide on a day-to-day basis. In this presentation we’ll sample a flavour of Parfait — we explore some real world challenges faced in the creation of a robust vulnerability detection tool, look into two examples of vulnerabilities that severely affected the Java platform in 2012/2013 and most machines in 2017/2018, and conclude by recounting what matters to developers for integration into today’s continuous integration and continuous delivery (CI/CD) pipelines.</p>
<p class="pn-title-2">Bio</p>
<p>Cristina is the Director of Oracle Labs Australia and an Architect at Oracle. Headquartered in Brisbane, the Lab focuses on Program Analysis as it applies to finding vulnerabilities in software and enhancing the productivity of developers worldwide. Prior to founding Oracle Labs Australia, Cristina was the Principal Investigator of the Parfait bug tracking project at Sun Microsystems, then Oracle.</p></div></div><br />
<div id="seminar-26" class="col-md-12 pn-seminar finished"><div id="kammar-user-defined-effects" class="pn-main-informations"><a onclick="return false;" class="pn-title">On the expressive power of user-defined effects</a>
<br />
<span class="pn-name">Ohad Kammar</span>
<span class="pn-affiliation">University of Oxford</span>
<a class="pn-url" target="_blank" href="https://www.cs.ox.ac.uk/people/ohad.kammar/main.html">https://www.cs.ox.ac.uk/people/ohad.kammar/main.html</a>
<br />
<span class="pn-datetime">3 October, 2018 10:00AM <a href="#kammar-user-defined-effects"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Computational effects, such as mutable state, memory allocation, non-determinism, and I/O interaction, allow programs to implicitly exhibit complex behaviour. I will discuss three abstractions that allow programmers to extend a language with user-defined effects. Control operators (call-cc, shift/reset, etc.) are a well-established abstraction for user-defined effects, and I will consider the specific shift/dollar without answer-type-modification. Since the 90s, functional languages have used monads for user-defined effects, and I will consider Filinski's monadic reflection. In the last decade, the community started looking into Plotkin and Pretnar's handlers for algebraic effects (extensible effects in Haskell, OCaml multicore, the Eff, Frank, Koka, and Links programming languages) as a programming abstraction, and I will consider deep handlers without forwarding. I will compare the relative expressive power of these three abstractions using Felleisen's notion of macro-translations. This comparison demonstrates the sensitivity of relative expressiveness of user-defined effects to seemingly orthogonal language features. This talk is based on the paper: On the expressive power of user-defined effects: effect handlers,monadic reflection, delimited control. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming, PACMPL 1(ICFP): 13:1-13:29 (2017),arXiv:1610.09161, DOI: 10.1145/3110257.</p>
<p class="pn-title-2">Bio</p>
<p>Ohad Kammar is a postdoctoral research associate at the University of Oxford Department of Computer Science, a Career Development Fellow at Balliol College Oxford, and an incoming Royal Society University Research Fellow at the University of Edinburgh School of Informatics. His fields of interests include programming language modelling and design, logic, and the foundations of computer science.</p></div></div><br />
<div id="seminar-27" class="col-md-12 pn-seminar finished"><div id="pedersen-trashtreasure" class="pn-main-informations"><a onclick="return false;" class="pn-title">From trash to treasure: Timing-sensitive garbage collection</a>
<br />
<span class="pn-name">Mathias Pedersen</span>
<span class="pn-affiliation">Aarhus University</span>
<a class="pn-url" target="_blank" href="http://cs.au.dk/~mvp/">http://cs.au.dk/~mvp/</a>
<br />
<span class="pn-datetime">19 September, 2018 10:00AM <a href="#pedersen-trashtreasure"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>We study information flows arising from timing channels in the presence of automatic memory management. We construct a series of example attacks that illustrate how garbage collectors form a shared resource that can be used to reliably leak sensitive information at a rate of up to 1 byte/sec on a contemporary general-purpose computer. The created channel is also observable across a network connection in a datacenter-like setting. We subsequently present a design of an automatic memory management system and prove that the presented attacks are impossible on garbage collectors satisfying this design. The guarantees provided by the language has been mechanized in the Coq proof assistant.</p>
<p class="pn-title-2">Bio</p>
<p>Mathias is a third year PhD student in the Logic and Semantics group at Aarhus University in Denmark, advised by Aslan Askarov. His work is in the area of language-based security, with a focus on provable mitigation of side channels. In general, anything related to compilers and the semantics of programming languages will be on his list of interests.</p></div></div><br />
<div id="seminar-28" class="col-md-12 pn-seminar finished"><div id="pombrio-infer-type-sugar" class="pn-main-informations"><a onclick="return false;" class="pn-title">Inferring Type Rules for Syntactic Sugar</a>
<br />
<span class="pn-name">Justin Pombrio</span>
<span class="pn-affiliation">Brown University</span>
<a class="pn-url" target="_blank" href="http://justinpombrio.net">http://justinpombrio.net</a>
<br />
<span class="pn-datetime">7 August, 2018 11:30AM <a href="#pombrio-infer-type-sugar"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Type systems and syntactic sugar are both valuable to programmers, but sometimes at odds. While sugar is a valuable mechanism for implementing realistic languages, the expansion process obscures program source structure. As a result, type errors can reference terms the programmers did not write (and even constructs they do not know), baffling them. The language developer must also manually construct type rules for the sugars, to give a typed account of the surface language. We address these problems by presenting a process for automatically reconstructing type rules for the surface language using rules for the core. We have implemented this theory, and show several interesting case studies.</p>
<p class="pn-title-2">Bio</p>
<p>Justin Pombrio is a recent PhD graduate from Brown University. His research is mainly in programming languages, with a focus on syntactic sugar, but also includes CS education.</p></div></div><br />
<div id="seminar-29" class="col-md-12 pn-seminar finished"><div id="nardelli-debug-debug" class="pn-main-informations"><a onclick="return false;" class="pn-title">Debugging Debug Information and Beyond</a>
<br />
<span class="pn-name">Francesco Zappa Nardelli</span>
<span class="pn-affiliation">Inria Paris – Rocquencourt</span>
<a class="pn-url" target="_blank" href="http://www.di.ens.fr/~zappa/">http://www.di.ens.fr/~zappa/</a>
<br />
<span class="pn-datetime">15 June, 2018 10:00AM <a href="#nardelli-debug-debug"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The spectacular results achieved by computer science in the recent years rely on hidden, obscure, and badly specified components that lurk at the very heart of our computing infrastructure. Consider DWARF debug information. Debug information is relied upon by debuggers and plays a key role in the in the implementation of program analysis tools. More surprisingly, debug information can be relied upon by the runtime of high-level programming languages, for instance by C++ to unwind the stack and implement exceptions. The debug information itself can be pervaded by subtle bugs, making the whole infrastructure unreliable. In this talk I will describe techniques and tools to perform validation and synthesis of the DWARF stack unwinding tables. I will also report on adventurous projects that we might build on top of reliable DWARF information.</p>
<p class="pn-title-2">Bio</p>
<p>Francesco Zappa Nardelli is a Researcher at Inria Paris – Rocquencourt. His research interests focus on concurrent computation on top of relaxed memory models, ranging from hardware models of modern architectures to high-level programming language specification and compilation. He received his Ph.D. from Université Paris 7 in 2003. Since then, he has worked on language design for distributed computation, type systems for integrating typed and untyped code in scripting languages, and tool support for semantics (including the Ott tool).</p></div></div><br />
<div id="seminar-30" class="col-md-12 pn-seminar finished"><div id="new-cbn-gtt" class="pn-main-informations"><a onclick="return false;" class="pn-title">Call-By-Name Gradual Type Theory</a>
<br />
<span class="pn-name">Max New</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://maxsnew.github.io/">http://maxsnew.github.io/</a>
<br />
<span class="pn-datetime">27 April, 2018 11:30AM <a href="#new-cbn-gtt"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>I will present Call-by-name (CBN) Gradual Type Theory [1], an axiomatic semantics of CBN gradual typing that directly axiomatizes the extensionality (eta) principles of types and the "gradual guarantee" of [2]. By axiomatizing the "term precision" relation of [2] we can provide a specification for casts as meets and joins with respect to precision. Using our type theory, we then show that the classic function contract ([3]) is in fact the unique implementation of function casts that satisfies extensionality and the gradual guarantee. This shows that the combination of these properties is a very strong constraint on the design of a gradually typed language and any implementation that departs must sacrifice one of these properties (typically extensionality).</p><p>[1] Call-by-Name Gradual Type Theory, New and Licata, to appear FSCD '18,https://arxiv.org/abs/1802.00061</p><p>[2] Refined Criteria for Gradual Typing, Siek, Vitousek, Cimini and Boyland, SNAPL '15, http://drops.dagstuhl.de/opus/volltexte/2015/5031/</p><p>[3] Contracts for Higher-Order Functions, Findler and Felleisen, ICFP '02,https://dl.acm.org/citation.cfm?id=581484</p>
<p class="pn-title-2">Bio</p>
<p>Max New is a PhD student at Northeastern University working on the semantic foundations of programming languages. He hates proving the same theorem twice and you should too.</p></div></div><br />
<div id="seminar-31" class="col-md-12 pn-seminar finished"><div id="tristan-probabilistic" class="pn-main-informations"><a onclick="return false;" class="pn-title">Compilation of Simple Probabilistic Programs to Gibbs Sampling.</a>
<br />
<span class="pn-name">John Tristan</span>
<span class="pn-affiliation">Oracle Labs</span>
<a class="pn-url" target="_blank" href="https://jtristan.github.io/">https://jtristan.github.io/</a>
<br />
<span class="pn-datetime">10 April, 2018 11:45AM <a href="#tristan-probabilistic"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>One of the several interesting challenges of probabilistic programming is that of compiling probabilistic programs to inference algorithms. One of these inference algorithms, Gibbs sampling, is particularly relevant because it is often statistically efficient, but unfortunately, it is difficult to derive and therefore compile to.</p> <p>In this talk, after a brief explanation of probabilistic programming and why its relevance to data science, I will explain some of the ideas behind the design of a compiler from (very) simple probabilistic programs to Gibbs sampling. I will also attempt to explain what it would mean for such a compiler to be correct.</p>
<p class="pn-title-2">Bio</p>
<p>Jean-Baptiste Tristan is a researcher in the machine learning group at Oracle Labs. He holds a Ph.D. in Computer Science from the French Institute for Research in Computer Science and Automation (INRIA) and a M.Sc. in Computer Science from the Ecole Normale Superieure of Paris.</p></div></div><br />
<div id="seminar-32" class="col-md-12 pn-seminar finished"><div id="alexandrescu-introspection" class="pn-main-informations"><a onclick="return false;" class="pn-title">Design by Introspection using the D Language</a>
<br />
<span class="pn-name">Andrei Alexandrescu</span>
<span class="pn-affiliation">D Language Foundation</span>
<a class="pn-url" target="_blank" href="http://erdani.com">http://erdani.com</a>
<br />
<span class="pn-datetime">6 February, 2018 11:45AM <a href="#alexandrescu-introspection"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Years ago, D started modestly as an improved offering in the realm of systems programming languages, sharing a good deal of philosophy with C and C++. With time, however, D became a very distinct language with unique features (and, of course, its own mistakes).</p><p>One angle of particular interest has been D's ability to perform compile-time introspection. Artifacts in a D program can be "looked at" during compilation. Coupled with a full-featured compile-time evaluation engine and with an ability to generate arbitrary code during compilation, this has led to a number of interesting applications.</p><p>This talk shares early experience with using these features of the D language. Design by Introspection is a proposed programming paradigm that assembles designs by performing introspection on components during compilation.</p>
<p class="pn-title-2">Bio</p>
<p>Andrei Alexandrescu is a researcher, software engineer, and author. He wrote three best-selling books on programming (Modern C++ Design, C++ Coding Standards, and The D Programming Language) and numerous articles and papers on wide-ranging topics from programming to language design to Machine Learning to Natural Language Processing. Andrei holds a PhD in Computer Science from the University of Washington and a BSc in Electrical Engineering from University "Politehnica" Bucharest. He currently works on the D Language Foundation. http://erdani.com</p></div></div><br />
<div id="seminar-33" class="col-md-12 pn-seminar finished"><div id="aref-declarative" class="pn-main-informations"><a onclick="return false;" class="pn-title">Solver-Aided Declarative Programming</a>
<br />
<span class="pn-name">Molham Aref</span>
<span class="pn-affiliation">Relational AI</span>
<a class="pn-url" target="_blank" href="#">#</a>
<br />
<span class="pn-datetime">14 December, 2017 10:00AM <a href="#aref-declarative"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>I will summarize our work on a declarative programming language that offers native language support for model (or instance) finding. This capability can be used to express predictive (e.g. machine learning) and prescriptive (e.g. combinatorial optimization) analytics. The presentation gives an overview of the platform and the language. In particular, it focuses on the important role of integrity constraints,which are used not only for maintaining data integrity, but also, for the formal specification of complex optimization problems and probabilistic programming.</p>
<p class="pn-title-2">Bio</p>
<p>Mr. Molham Aref is the Chief Executive Officer of Relational AI. Mr. Aref has more than 25 years of experience in developing and implementing enterprise-grade analytic, predictive, optimization and simulation solutions for the demand chain, supply chain, and revenue management across various industries. Relational AI combines the latest advances in Artificial Intelligence with a understanding of business processes to develop solutions that shape better decisions, improve agility, and reduce risk. Prior to Relational AI, he was co-founder and CEO of LogicBlox where he led the company from inception through a successful sale to Infor. Previously, he was CEO of Optimi (acquired by Ericsson),a leader in wireless network simulation and optimization, and co-founder of Brickstream (renamed Nomi and then acquired by FLIR), a leading provider of computer-vision-based behavior intelligence solutions.</p></div></div><br />
<div id="seminar-34" class="col-md-12 pn-seminar finished"><div id="martens-compositional" class="pn-main-informations"><a onclick="return false;" class="pn-title">Compositional Creativity</a>
<br />
<span class="pn-name">Chris Martens</span>
<span class="pn-affiliation">North Carolina State University</span>
<a class="pn-url" target="_blank" href="https://sites.google.com/ncsu.edu/cmartens">https://sites.google.com/ncsu.edu/cmartens</a>
<br />
<span class="pn-datetime">11 December, 2017 11:00AM <a href="#martens-compositional"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Creativity is seen as a core cognitive ability for tasks like storytelling, conversation, and aesthetic design. Simulating creative processes with computers enables them to amplify humans' natural creativity and to support applications like interactive narrative, chatbots, and procedural level generators for games. By now, a large number of techniques exist for simulating creativity, such as search, planning, production grammars, logic programming, stochastic modeling from data, and hybrid approaches. However, even the simplest methods are commonly considered programming tasks for "AI experts." High-level programming languages have the potential to broaden participation in authorship of these systems, but only if they are designed with compositionality -- the mathematical principle that's also functional programming's secret weapon -- in mind. This talk will discuss what compositionality has achieved so far for creative computing and what we can do with it next.</p>
<p class="pn-title-2">Bio</p>
<p>Chris Martens is an assistant professor in the Computer Science (CSC) Department at NC State, where she is affiliated with the Digital Games research group. Her interests span artificial intelligence, programming languages, and formal methods.</p></div></div><br />
<div id="seminar-35" class="col-md-12 pn-seminar finished"><div id="muehlboeck-nom" class="pn-main-informations"><a onclick="return false;" class="pn-title">Efficient Nominal Gradual Typing</a>
<br />
<span class="pn-name">Fabian Muehlboeck</span>
<span class="pn-affiliation">Cornell University</span>
<a class="pn-url" target="_blank" href="http://www.cs.cornell.edu/~fabianm/">http://www.cs.cornell.edu/~fabianm/</a>
<br />
<span class="pn-datetime">5 December, 2017 2:00PM <a href="#muehlboeck-nom"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Gradual Typing is the idea that we can support both static and dynamic type checking in different parts of the same program in the same language. Most existing work on gradual typing aims to add gradual typing to an existing language. However, this severely constrains some key decisions in creating gradually typed languages, often leading designers to trade off either soundness or efficiency.</p>
<p>I will talk about designing a nominal object-oriented language with gradual typing as a core component from the start. This affects key design decisions for the other type system features, as well as the design of the runtime. Experiments with a prototype language I implemented suggest that this is a viable approach to achieve sound, yet efficient gradual typing. I will present those results and talk about some key design challenges that have yet to be solved.</p>
<p class="pn-title-2">Bio</p>
<p>Fabian Muehlboeck is a Ph.D. student working with Ross Tate at Cornell University.</p></div></div><br />
<div id="seminar-36" class="col-md-12 pn-seminar finished"><div id="siskand-cps" class="pn-main-informations"><a onclick="return false;" class="pn-title">What does CPS have to do with deep learning?</a>
<br />
<span class="pn-name">Jeffrey M. Siskind</span>
<span class="pn-affiliation">Purdue University</span>
<a class="pn-url" target="_blank" href="https://engineering.purdue.edu/~qobi/">https://engineering.purdue.edu/~qobi/</a>
<br />
<span class="pn-datetime">11 September, 2017 1:30PM <a href="#siskand-cps"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Deep learning is formulated around backpropagation, a method for computing gradients of a particular class of data flow graphs to train models to minimize error by gradient descent. Backpropagation is a special case of a more general method known as reverse mode automatic differentiation (AD) for computing gradients of functions expressed as programs. Reverse mode AD imposes only a small constant-factor overhead in operation count over the original computation, but has storage requirements that grow, in the worst case, in proportion to the time consumed by the original computation. This storage blowup can be ameliorated by check pointing, a process that reorders application of classical reverse-mode AD over an execution interval to tradeoff space vs. time. Application of check pointing in a divide-and-conquer fashion to strategically chosen nested execution intervals can break classical reverse-mode AD into stages which can reduce the worst-case growth in storage from linear to logarithmic. Doing this has been fully automated only for computations of particularly simple form, with checkpoints spanning execution intervals resulting from a limited set of program constructs. We show how the technique can be automated for arbitrary computations. Doing so relies on implementing general purpose mechanisms for counting the number of instructions executed by a program, interrupting the execution after a specified number of steps, and resuming the execution with a nonstandard interpretation. We implement these general purpose mechanisms with a compiler that converts programs to continuation-passing style (CPS). The process of efficiently computing gradients with check pointing requires running, and rerunning, little bits of the program out of order. This is made easier by applying the technique to functional programs. There is a deeper and higher-level message in this talk: machine learning can benefit from advanced techniques from programming language theory.</p>
<p class="pn-title-2">Bio</p>
<p>Jeffrey M. Siskind received the B.A. degree in Computer Science from the Technion, Israel Institute of Technology, Haifa, in 1979, the S.M. degree in Computer Science from the Massachusetts Institute of Technology (M.I.T.), Cambridge, in 1989, and the Ph.D. degree in Computer Science from M.I.T. in 1992. He did a postdoctoral fellowship at the University of Pennsylvania Institute for Research in Cognitive Science from 1992 to 1993. He was an assistant professor at the University of Toronto Department of Computer Science from 1993 to 1995, a senior lecturer at the Technion Department of Electrical Engineering in 1996, a visiting assistant professor at the University of Vermont Department of Computer Science and Electrical Engineering from 1996 to 1997, and a research scientist at NEC Research Institute, Inc. from 1997 to 2001. He joined the Purdue University School of Electrical and Computer Engineering in 2002 where he is currently an associate professor. His research interests include computer vision, robotics, artificial intelligence, neuroscience, cognitive science, computational linguistics, child language acquisition, automatic differentiation, and programming languages and compilers.</p></div></div><br />
<div id="seminar-37" class="col-md-12 pn-seminar finished"><div id="jamner-gradual" class="pn-main-informations"><a onclick="return false;" class="pn-title">Relational Parametricity for Polymorphic Blame Calculus</a>
<br />
<span class="pn-name">Dustin Jamner</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="https://github.com/DIJamner">https://github.com/DIJamner</a>
<br />
<span class="pn-datetime">23 June, 2017 12:00PM <a href="#jamner-gradual"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this work we prove that the polymorphic blame calculus satisfies relational parametricity. The proof relies on a step-indexed Kripke logical relation. The step-indexing is required to make the logical relation well-defined in the case for the dynamic type. The possible worlds include the mapping of generated type names to their concrete types and the mapping of type names to relations. We prove the Fundamental Property of this logical relation and that it is sound with respect to contextual equivalence.</p>
<p class="pn-title-2">Bio</p>
<p>Dustin Jamner is an undergraduate at Northeastern University in Computer Science, working with Amal Ahmed.</p></div></div><br />
<div id="seminar-38" class="col-md-12 pn-seminar finished"><div id="tinelli-cocospec" class="pn-main-informations"><a onclick="return false;" class="pn-title">CoCoSpec: A Mode-aware Contract Language for Reactive Systems</a>
<br />
<span class="pn-name">Cesare Tinelli</span>
<span class="pn-affiliation">University of Iowa</span>
<a class="pn-url" target="_blank" href="http://homepage.cs.uiowa.edu/~tinelli/">http://homepage.cs.uiowa.edu/~tinelli/</a>
<br />
<span class="pn-datetime">1 June, 2017 11:00AM <a href="#tinelli-cocospec"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Contract-based software development is a leading methodology for the construction of safety- and mission-critical embedded systems. Contracts are an effective way to establish boundaries between components and can be used efficiently to verify global properties by using compositional reasoning techniques. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Requirements in the specification of a component are often case-based, with each case describing what the component should do depending on a specific situation (or mode) the component is in.</p><p>This talk introduces CoCoSpec, a mode-aware assume-guarantee-based contract language for embedded systems. CoCoSpec is built as an extension of the Lustre language and lets users specify mode behavior directly, instead of encoding it as conditional guarantees, thus preventing a loss of mode-specific information. Mode-aware model checkers supporting CoCoSpec can increase the effectiveness of the compositional analysis techniques found in assume-guarantee frameworks and improve scalability. Such tools can also produce much better feedback during the verification process, as well as valuable qualitative information on the contract itself. I will presents the CoCoSpec language and illustrate the benefits of mode-aware model-checking on a case study involving a flight-critical avionics system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based model checker developed at the University of Iowa that provides full support for CoCoSpec.</p>
<p class="pn-title-2">Bio</p>
<p>Cesare Tinelli received a Ph.D. in Computer Science from the UIUC in 1999 and is currently a professor in Computer Science at the University of Iowa. His research interests include automated reasoning and formal methods. He has done seminal work in automated reasoning, in particular in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. His work has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, and NSF) and corporations (Intel, General Electric, Rockwell Collins, and United Technologies) and has appeared in more than 70 refereed publications. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He has led the development of the award winning Darwin theorem prover and the Kind model checker. He co-leads the development of CVC4,a widely used and award winning SMT solver, and StarExec, a cross community web-based service for the comparative evaluation of logic solvers.</p></div></div><br />
<div id="seminar-39" class="col-md-12 pn-seminar finished"><div id="linear-experiment" class="pn-main-informations"><a onclick="return false;" class="pn-title">Multi-language programming system: a linear experiment</a>
<br />
<span class="pn-name"></span>
<span class="pn-affiliation"></span>
<a class="pn-url" target="_blank" href=""></a>
<br />
<span class="pn-datetime">5 May, 2017 12:00PM <a href="#linear-experiment"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Programming language research keeps inventing more powerful dynamic and static features for programming language. Ideally, thorough language design should be able to propose a single, unified, powerful yet simple view of them as orthogonal aspects of a single programming language that would remain usable by everyone. In practice, it always takes much more time and effort to find the simple/orthogonal presentation than to come up with the desirable features, and we become emotionally attached to programming language monoliths (C++, Scala, GHC Haskell, OCaml, Common Lisp...) that suffer from feature creep. An alternative is to design programming systems as multi-language environment instead. This point of view makes it easier to detect flaws in a proposed programming system design: there is no clear objective definition of what "orthogonal features" really mean, but we have clear ideas of how multi-language systems should work. The Racket Manifesto says: "Each language and component must be able to protect its specific invariants".</p><p>In this work we give a formal specification, in terms of full abstraction, for what it means for a new language added to the system to not introduce "abstraction leaks" in the other languages, and discuss scenarios where this translates in (informal) usability properties: having a nice teachable language subset, or gracefully introducing an advanced language for experts. We present a multi-language design that exhibits this formal property by adding a language L with linear types and linear state to a typical ML-style programming language U. L allows to write programs with resource usage guarantees (space consumption, typestate-style safety guarantees) that were not possible in U, without introducing abstraction leaks. We will demonstrate several useful examples, some of them that crucially rely on the fine-grained use of language boundaries, at a subterm level rather than whole-module level.</p>
<p class="pn-title-2">Bio</p>
<p></p></div></div><br />
<div id="seminar-40" class="col-md-12 pn-seminar finished"><div id="madsen-flix" class="pn-main-informations"><a onclick="return false;" class="pn-title">From Datalog to Flix: A Declarative Language for Fixed Points on Lattices</a>
<br />
<span class="pn-name">Magnus Madsen</span>
<span class="pn-affiliation">University of Waterloo</span>
<a class="pn-url" target="_blank" href="plg.uwaterloo.ca/~mmadsen/">plg.uwaterloo.ca/~mmadsen/</a>
<br />
<span class="pn-datetime">14 April, 2017 1:30PM <a href="#madsen-flix"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>We present FLIX, a declarative programming language for specifying and solving least fixed point problems, particularly static program analyses. FLIX is inspired by Datalog and extends it with lattices and monotone functions. Using FLIX,implementors of static analyses can express a broader range of analyses than is currently possible in pure Datalog, while retaining its familiar rule-based syntax. We define a model-theoretic semantics of FLIX as a natural extension of the Datalog semantics. This semantics captures the declarative meaning of FLIX programs without imposing any specific evaluation strategy. An efficient strategy is semi-naïve evaluation which we adapt for FLIX. We have implemented a compiler and runtime for FLIX, and used it to express several well-known static analyses, including the IFDS and IDE algorithms. The declarative nature of FLIX clearly exposes the similarity between these two algorithms.</p> <p>This work has previously been presented at PLDI 2016. The talk will cover some of that material as well as recent developments.</p>
<p class="pn-title-2">Bio</p>
<p>The speaker is a post doctoral fellow at the University of Waterloo.</p></div></div><br />
<div id="seminar-41" class="col-md-12 pn-seminar finished"><div id="sagiv-protocols" class="pn-main-informations"><a onclick="return false;" class="pn-title">Simple Invariants for proving the safety of distributed protocols and networks</a>
<br />
<span class="pn-name">Mooly Sagiv</span>
<span class="pn-affiliation">Tel Aviv University</span>
<a class="pn-url" target="_blank" href="http://www.cs.tau.ac.il/~msagiv/">http://www.cs.tau.ac.il/~msagiv/</a>
<br />
<span class="pn-datetime">31 March, 2017 12:00PM <a href="#sagiv-protocols"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Safety of a distributed protocol means that the protocol never reaches a bad state, e.g., a state where two nodes become leaders in a leader-election protocol. Proving safety is obviously undecidable since such protocols are run by an unbounded number of nodes, and their safety needs to be established for any number of nodes. I will describe a deductive approach for proving safety, based on the concept of universally quantified inductive invariants --- an adaptation of the mathematical concept of induction to the domain of programs. In the deductive approach, the programmer specifies a candidate inductive invariant and the system automatically checks if it is inductive. By restricting the invariants to be universally quantified, this approach can be effectively implemented with a SAT solver.</p><p>This is a joint work with Ken McMillan (MSR), Oded Padon (TAU), Aurojit Panda(Berkeley) , and Sharon Shoham(TAU) and was integrated into the IVY system: http://www.cs.tau.ac.il/~odedp/ivy/. The work is inspired by Shachar Itzhaky's thesis available from http://people.csail.mit.edu/shachari/</p>
<p class="pn-title-2">Bio</p>
<p>Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv University. He is a leading researcher in the area of large scale (inter-procedural) program analysis, and one of the key contributors to shape analysis. His fields of interests include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments. Sagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition. Prof. Sagiv served as Member of the Advisory Board of Panaya Inc acquired by Infosys. He received best-paper awards at PLDI'11 and PLDI'12 for his work on composing concurrent data structures and a ACM SIGSOFT Retrospective Impact Paper Award (2011) for program slicing. He is an ACM fellow and a recipient of Microsoft Research Outstanding Collaborator Award 2016.</p></div></div><br />
<div id="seminar-42" class="col-md-12 pn-seminar finished"><div id="chaudhuri-automatic" class="pn-main-informations"><a onclick="return false;" class="pn-title">Learning to Program and Debug, Automatically</a>
<br />
<span class="pn-name">Swarat Chaudhuri</span>
<span class="pn-affiliation">Rice University</span>
<a class="pn-url" target="_blank" href="https://www.cs.rice.edu/~sc40/">https://www.cs.rice.edu/~sc40/</a>
<br />
<span class="pn-datetime">24 March, 2017 12:00PM <a href="#chaudhuri-automatic"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Automating programming and debugging are long-standing goals in computer science. In spite of significant progress in formal methods over the years, we remain very far from achieving these goals. For example, a freshman CS major will typically program circles around today's best program synthesizers. Debugging and verification tools rely on formal specifications, which are hard to provide in many important applications.</p><p>Two critical components of the gap between human and machine programmers are that humans learn from experience, i.e., data, and can easily generalize from incomplete problem definitions. In this talk, I will present a general framework for formal methods, based on Bayesian statistical learning, that aims to eliminate these differences. In our framework, descriptions of programming tasks are seen to be "clues" towards a hidden (probabilistic) specification that fully defines the task. Large corpora of real-world programs are used to construct a statistical model that correlates specifications with the form and function of their implementations. The framework can be implemented in a variety of ways, but in particular, through a neural architecture called Bayesian variational encoder-decoders. Inferences made using the framework can be used to guide traditional algorithms for program synthesis and bug-finding.</p><p>I will show that this data-driven approach can lead to giant leaps in the scope and performance of automated program synthesis and debugging algorithms. Specifically, I will give a demo of Bayou, a system for Bayesian inductive synthesis of Java programs that goes significantly beyond the state of the art in program synthesis. I will also describe Salento, a debugging system based on our framework that can find subtle violations of API contracts without any kind of specification.</p>
<p class="pn-title-2">Bio</p>
<p>Swarat Chaudhuri is an Associate Professor of Computer Science at Rice University. His research lies at the interface of programming systems and artificial intelligence. Much of his recent work is on program synthesis, the problem of automatically generating computer programs from high-level specifications.</p></div></div><br />
<div id="seminar-43" class="col-md-12 pn-seminar finished"><div id="hartzell-templates" class="pn-main-informations"><a onclick="return false;" class="pn-title">Templates and Types in C++</a>
<br />
<span class="pn-name">Jimmy Hartzell</span>
<span class="pn-affiliation">Tower Research</span>
<a class="pn-url" target="_blank" href=""></a>
<br />
<span class="pn-datetime">10 March, 2017 12:00PM <a href="#hartzell-templates"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Like many modern programming languages, C++ supports both generic
programming (templates) and object-oriented programming (inheritance and
virtual functions). Unlike many modern programming languages, the generic
programming mechanism does not fully leverage or interact with the type
system. It amounts to compile-time duck typing: C++ function templates,
like functions from a non-statically typed programming language, have
their full interface implicit in their implementations -- making it hard
to discern what that interface actually is. The concept of Concepts
(compile-time typeclasses) was slated for introduction into C++ in
the C++11 version of the standard, then C++14, then C++17, now C++20... What can
we do to work around their absence?</p><p>Relatedly, how do we bridge the gap
between static and dynamic polymorphism? C++ provides both, and sometimes we
want to mix and mash them. Template tricks can also be done to accomplish this
as well.</p>
<p class="pn-title-2">Bio</p>
<p>Jimmy Hartzell is a software developer and C++ instructor at Tower Research.</p></div></div><br />
<div id="seminar-44" class="col-md-12 pn-seminar finished"><div id="sherman-patterns" class="pn-main-informations"><a onclick="return false;" class="pn-title">Overlapping pattern matching for programming with continuous functions</a>
<br />
<span class="pn-name">Ben Sherman</span>
<span class="pn-affiliation">MIT</span>
<a class="pn-url" target="_blank" href="http://www.ben-sherman.net/">http://www.ben-sherman.net/</a>
<br />
<span class="pn-datetime">24 February, 2017 12:00PM <a href="#sherman-patterns"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room">| <a class="pn-url" target="_blank" href="https://github.com/nuprl/website/blob/master/seminar-notes/sherman-patterns.md">Notes</a></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Topology, when viewed from an unusual perspective (formal topology), describes how to compute with certain objects that are beyond the reach of induction, such as real numbers, probability distributions, streams, and function spaces. Accordingly, one gets a programming language whose types are spaces and whose functions are continuous maps.</p><p>Does this language have pattern matching? In functional programming, pattern matching allows definition of a function by partitioning the input and defining the result in each case. We generalize to programming with spaces, where patterns need not represent decidable predicates and also may overlap, potentially allowing nondeterministic behavior in overlapping regions. These overlapping pattern matches are useful for writing a wide array of computer programs on spaces, such as programs that make approximate computations or decisions based on continuous values or that manipulate "partial" datatypes.</p><p>This talk will introduce topology from a computational perspective, and explore some programs that can be built with this framework using overlapping pattern matching.</p>
<p class="pn-title-2">Bio</p>
<p>Ben Sherman is a second-year PhD student at MIT, advised by Adam Chlipala and Michael Carbin.</p></div></div><br />
<div id="seminar-45" class="col-md-12 pn-seminar finished"><div id="belyakova-oo" class="pn-main-informations"><a onclick="return false;" class="pn-title">Comparative Study of Generic Programming Features in Object-Oriented Languages</a>
<br />
<span class="pn-name">Julia Belyakova</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://staff.mmcs.sfedu.ru/~juliet/index.en.html">http://staff.mmcs.sfedu.ru/~juliet/index.en.html</a>
<br />
<span class="pn-datetime">3 February, 2017 12:00PM <a href="#belyakova-oo"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Earlier comparative studies of language support for generic programming (GP) have shown that mainstream object-oriented (OO) languages such as C# and Java provide weaker support for GP as compared with functional languages such as Haskell or SML.</p><p>One reason is that generic mechanisms of C# and Java are based on F-bounded polymorphism, which has certain deficiencies. Some of these deficiencies are eliminated in more recent languages, such as Scala and Kotlin. However, there are peculiarities of object-oriented languages as a whole, which prevent them from being as expressible as Haskell in terms of generic programming.</p><p>In this talk we will cover the main problems of language support for generic programming in C#/Java as well as other modern object-oriented languages, including Scala and Swift. It turns out that all of these languages follow the same approach to constraining type parameters, which leads to inevitable shortcomings. To overcome them, an alternative approach is suggested in several extensions for OO languages, in particular, JavaGenus. The advantages and drawbacks of both approaches will be discussed in the talk.</p><p>Here are Julia's <a href="http://staff.mmcs.sfedu.ru/~juliet/files/materials/seminar-talks/belyakova-PL-sem-2017-slides.pdf">Slides</a>.</p>
<p class="pn-title-2">Bio</p>
<p>Julia Belyakova graduated in 2014 from Southern Federal University (Rostov-on-Don, Russia) as Master of Science in “Computer Science and Information Technologies”. She is enrolled for PhD program in Southern Federal University and came to Northeastern University as a visiting scientist. She is currently doing research in the area of generic programming for object-oriented languages.</p></div></div><br />
<div id="seminar-46" class="col-md-12 pn-seminar finished"><div id="vilk-browsers" class="pn-main-informations"><a onclick="return false;" class="pn-title">Making the Browser Reasonable for Sane Programmers</a>
<br />
<span class="pn-name">John Vilk</span>
<span class="pn-affiliation">University of Massachusetts Amherst</span>
<a class="pn-url" target="_blank" href="https://jvilk.com/">https://jvilk.com/</a>
<br />
<span class="pn-datetime">27 January, 2017 12:00PM <a href="#vilk-browsers"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Billions of people use browsers to access the web from a variety of devices, but it remains difficult to write and debug the client-side of web applications. The browser exposes unfamiliar, redundant, and incompatible abstractions for a variety of common tasks, preventing developers from adapting existing code written for other platforms. The browser environment is completely event-driven and pervasively concurrent, resulting in complex control flow and race conditions that are difficult to debug.</p><p>In this talk, I will describe how my research makes it easier to write and debug web applications. Doppio is a JavaScript runtime system that lets developers run unaltered code written in general-purpose languages, such as Java and C/C++, directly inside the browser. Browsix further enhances Doppio with a kernel, processes, and shared operating system resources, letting multiple off-the-shelf programs concurrently interoperate on the same webpage. ReJS is a low-overhead and high-fidelity time-traveling debugger that lets developers instantaneously step forward and backward through a program's execution. ReJS accurately recreates the application's complete behavior, including the GUI and multiple types of race conditions, while producing miniscule and portable application traces. These resources transform the browser into a first-class application platform.</p>
<p class="pn-title-2">Bio</p>
<p>John Vilk is a Ph.D. candidate in the College of Information and Computer Sciences at the University of Massachusetts Amherst. He is a member of the PLASMA lab, and is advised by Emery Berger. John's research aims to improve the browser as an application platform by making it easier to write, debug, and optimize complex web applications. John is a Facebook Fellow (2015), and his work on Doppio: Breaking the Browser Language Barrier is a SIGPLAN Research Highlight (2014) and a PLDI Distinguished Artifact (2014). His research forms the basis of Microsoft ChakraCore's time-traveling debugger and lets millions of people interact with legacy software and games in their browser at the Internet Archive (https://archive.org/). John received his MS from the University of Massachusetts Amherst (2013) and his BS from Worcester Polytechnic Institute (2011).</p><p>You can learn more about John at his website, https://jvilk.com/.</p></div></div><br />
<div id="seminar-47" class="col-md-12 pn-seminar finished"><div id="new-retractionsblame" class="pn-main-informations"><a onclick="return false;" class="pn-title">Retractions and Blame</a>
<br />
<span class="pn-name">Max New</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://maxsnew.github.io/">http://maxsnew.github.io/</a>
<br />
<span class="pn-datetime">15 December, 2016 12:00PM <a href="#new-retractionsblame"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">Behrakis 105</span>
<span class="pn-room">| <a class="pn-url" target="_blank" href="https://github.com/nuprl/website/blob/master/seminar-notes/new-retractionsblame.md">Notes</a></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>It has long been noted that research on contracts and gradual typing bears a striking resemblance to Dana Scott's work on retracts in domain theory. However, a concrete relationship has been elusive, especially since the notion of *blame* has seemingly no counterpart in domain theory.</p><p>We connect these fields by means of gradual type precision, which has been characterized previously using blame in [1]. We propose a definition in terms of section-retraction pairs, allowing us to relate blame and retractions in a precise way. Our definition agrees with [1] on most rules, but differs in a way that suggests a modification to their definition of blame.</p><p>[1] Wadler and Findler, Well-typed Programs can't Be Blamed:
http://homepages.inf.ed.ac.uk/wadler/topics/blame.html#blame-esop</p>
<p class="pn-title-2">Bio</p>
<p>Max New is a PhD student at Northeastern University working on the semantic foundations of programming languages. He hates proving the same theorem twice and you should too.</p></div></div><br />
<div id="seminar-48" class="col-md-12 pn-seminar finished"><div id="scherer-emptytype" class="pn-main-informations"><a onclick="return false;" class="pn-title">Deciding program equivalence with sums and the empty type</a>
<br />
<span class="pn-name">Gabriel Scherer</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://www.ccs.neu.edu/home/gasche/">http://www.ccs.neu.edu/home/gasche/</a>
<br />
<span class="pn-datetime">7 December, 2016 12:00PM <a href="#scherer-emptytype"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 110</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The simply-typed λ-calculus, with only function types, is strongly normalizing, and its program equivalence relation is decidable: unlike in more advanced type system with polymorphism or effects, the natural "syntactic" equivalence (βη-equivalence) corresponds to natural "semantic" equivalence (observational or contextual equivalence), and is decidable. Adding product types (pairs) is easy and preserves these properties, but sums (disjoint unions) are, surprisingly, harder. It is only in 1995 that Neil Ghani proved that the equivalence in presence of sums is decidable, and the situation in presence of the empty type (zero-ary sum) was unknown.</p><p>We propose an equivalence algorithm for sums and the empty type that takes inspiration from a proof-theoretic technique, named "focusing",designed for proof search. The exposition will be introductory; I will present the difficulties caused by sums and the empty type, present some of the existing approaches for sums in the literature, introduce focusing, and give a high-level intuition of our saturation-based algorithm and its termination argument. No previous knowledge of focusing is assumed. I expect some familiarity with typed lambda-calculi, but will recall all concepts used (for example, βη-equivalence) during the talk.</p>
<p class="pn-title-2">Bio</p>
<p>Gabriel is interested in theoretical aspects of type systems,
programming language implementation, general programming language
concepts, and even some syntactic aspects. He has a preference for the
formalizable aspects, or formalizable approaches to programming
language aspects, rather than the often subjective appeal to taste or
intuition.</p></div></div><br />
<div id="seminar-49" class="col-md-12 pn-seminar finished"><div id="dolby-wala" class="pn-main-informations"><a onclick="return false;" class="pn-title">Analysis of Android hybrid applications and other fun with WALA</a>
<br />
<span class="pn-name">Julian Dolby</span>
<span class="pn-affiliation">IBM Research</span>
<a class="pn-url" target="_blank" href="http://researcher.ibm.com/person/us-dolby">http://researcher.ibm.com/person/us-dolby</a>
<br />
<span class="pn-datetime">1 December, 2016 12:00PM <a href="#dolby-wala"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">Richards Hall 140</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Hybrid apps help developers build multiple apps for different platforms with less duplicated effort, by providing platform-specific functionality via native code and user interactions via javascript code. however, most hybrid apps are developed in multiple programming languages with different semantics, complicating programming. moreover, untrusted javascript code may access device-specific features via native code, exposing hybrid apps to attacks. Unfortunately, there are no existing tools to detect such vulnerabilities. In this paper, we present HybriDroid, the first static analysis framework for Android hybrid apps. First, we investigate the semantics of interoperation of Android Java and JavaScript. Then, we design and implement a static analysis framework that analyzes inter-communication between Android Java and JavaScript. We demonstrate HybriDroid with a bug detector that identifies programmer errors due to the hybrid semantics, and a taint analyzer that finds information leaks cross language boundaries. Our empirical evaluation shows that the tools are practically usable in that they found previously uncovered bugs in real-world Android hybrid apps and possible information leaks via a widely-used advertising platform.</p><p>The bulk of this presentation will focus on ASE 2016 work on analysis of hybrid apps (1), a blend of per-platform native code and portable JavaScript. I will also briefly discuss two other recent projects involving WALA: ASE 2015 work on a practically tunable static analysis framework for large-scale JavaScript applications (2), and ISSTA 2015 work on scalable and precise taint analysis for Android (3).</p><p>1: Sungho Lee, Julian Dolby, Sukyoung Ryu: HybriDroid: static analysis framework for Android hybrid applications. ASE 2016: 250-261</p><p>2: Yoonseok Ko, Hongki Lee, Julian Dolby, Sukyoung Ryu: Practically Tunable Static Analysis Framework for Large-Scale JavaScript Applications (T). ASE 2015: 541-551</p><p>3: Wei Huang, Yao Dong, Ana Milanova, Julian Dolby: Scalable and precise taint analysis for Android. ISSTA 2015: 106-117</p>
<p class="pn-title-2">Bio</p>
<p>Julian Dolby is a Research Staff Member at the IBM Thomas J. Watson Research Center, where he works on a range of topics, including static program analysis, software testing, concurrent programming models and the semantic Web. He is one of the primary authors of the publically available Watson Libraries for Analysis (WALA) program analysis infrastructure, and his recent WALA work has focused on creating the WALA Mobile infrastructure.</p><p>His program analysis work has recently focused on scripting languages like JavaScript and on security analysis of Web applications; this work has been included in IBM products, most notably Rational AppScan, Standard Edition and Source Edition. He was educated at the University of Illinois at Urbana-Champaign as a graduate student where he worked with Professor Andrew Chien on programming systems for massively-parallel machines.</p></div></div><br />
<div id="seminar-50" class="col-md-12 pn-seminar finished"><div id="ariola-sequent" class="pn-main-informations"><a onclick="return false;" class="pn-title">Sequent calculus as a programming language</a>
<br />
<span class="pn-name">Zena Ariola</span>
<span class="pn-affiliation">University of Oregon</span>
<a class="pn-url" target="_blank" href="http://ix.cs.uoregon.edu/~ariola/">http://ix.cs.uoregon.edu/~ariola/</a>
<br />
<span class="pn-datetime">28 November, 2016 12:00PM <a href="#ariola-sequent"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 110</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>We will present and demonstrate the usefulness of the sequent
calculus as a formal model of computation based on interactions
between producers and consumers of results. This model leads
to a better understanding of call-by-name evaluation by
reconciling the conflicting principles of extensionality and
weak-head evaluation, thus internalizing a known parametricity
result. It allows one to explore two dualities of computation:
the duality between call-by-name and call-by-value, and the
duality between construction and deconstruction. This ultimately
leads to a better linguistic foundation for co-induction as dual
to induction. From a more practical point of view, the sequent
calculus provides a useful inspiration for the design of
intermediate languages.</p>
<p class="pn-title-2">Bio</p>
<p>TBD</p></div></div><br />
<div id="seminar-51" class="col-md-12 pn-seminar finished"><div id="culpepper-probablistic" class="pn-main-informations"><a onclick="return false;" class="pn-title">Contextual Equivalence of Probabilistic Programs</a>
<br />
<span class="pn-name">Ryan Culpepper</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://www.ccs.neu.edu/home/ryanc/">http://www.ccs.neu.edu/home/ryanc/</a>
<br />
<span class="pn-datetime">3 November, 2016 12:00PM <a href="#culpepper-probablistic"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>In this talk I introduce a probabilistic programming language with continuous random variables and soft constraints, define contextual equivalence for the language, and then present a logical relation that is sound with respect to contextual equivalence.</p><p>The question of equivalence for probabilistic programs is interesting and difficult because the meaning of a program is a measure defined by integrating over the space of all of the program's possible evaluations. Thus creating a workable logical relation requires proving integral equalities involving intermediate measures that are ``equal enough'' but still respect contextual equivalence.</p>
<p class="pn-title-2">Bio</p>
<p>Ryan Culpepper is a research scientist at Northeastern University. He works on probabilistic programming as well as extensible languages and tools for building domain-specific languages. He received his PhD at Northeastern and did a postdoc at the University of Utah.</p></div></div><br />
<div id="seminar-52" class="col-md-12 pn-seminar finished"><div id="meiklejohn-computation" class="pn-main-informations"><a onclick="return false;" class="pn-title">Declarative, Convergent Edge Computation</a>
<br />
<span class="pn-name">Christopher Meiklejohn</span>
<span class="pn-affiliation">Université Catholique
de Louvain</span>
<a class="pn-url" target="_blank" href="https://christophermeiklejohn.com/">https://christophermeiklejohn.com/</a>
<br />
<span class="pn-datetime">27 October, 2016 12:00PM <a href="#meiklejohn-computation"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Consistency is hard and coordination is expensive. As we move into the
world of connected 'Internet of Things' style applications, or
large-scale mobile applications, devices have less power, periods of
limited connectivity, and operate over unreliable asynchronous
networks. This poses a problem with shared state: how do we handle
concurrent operations over shared state, while clients are offline,
and ensure that values converge to a desirable result without making
the system unavailable?</p>
<p>We look at a new programming model, called Lasp. This programming
model combines distributed convergent data structures with a dataflow
execution model designed for distribution over large-scale
applications. This model supports arbitrary placement of processing
node: this enables the user to author applications that can be
distributed across data centers and pushed to the edge.</p>
<p class="pn-title-2">Bio</p>
<p>Christopher Meiklejohn loves distributed systems and programming
languages. Previously, Christopher worked at Basho Technologies, Inc.
on the distributed key-value store, Riak. Christopher develops a
programming model for distributed computation, called Lasp.
Christopher is currently a Ph.D. student at the Université Catholique
de Louvain in Belgium.</p></div></div><br />
<div id="seminar-53" class="col-md-12 pn-seminar finished"><div id="verlaguet-hack" class="pn-main-informations"><a onclick="return false;" class="pn-title">The Hack Experiment & HHVM, Then And Now</a>
<br />
<span class="pn-name">Julien Verlaguet & Brett Simmers</span>
<span class="pn-affiliation">Facebook</span>
<a class="pn-url" target="_blank" href="http://hacklang.org/">http://hacklang.org/</a>
<br />
<span class="pn-datetime">25 October, 2016 1:30PM <a href="#verlaguet-hack"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The Hack programming language developed at Facebook is an evolution of PHP. With tens of millions of lines of PHP code in house, the lack of type and poor IDE support were felt to be major threats to Facebook. We designed Hack gradually, adding feature at regular intervals and encouraging developers to adopt them in their code. This talk will touch on the design of the Hack language, its type system, the implementation of the type checker, and the social processes involved in converting 20 millions lines of untyped code to a rich type system.</p><p>HHVM is an open source virtual machine for PHP and Hack programs. It was developed by Facebook but is also used by Wikipedia, Baidu, Etsy, and many others. This talk will discuss the history of the project, what goes on behind the scenes while executing your PHP code, and what we're currently working on.</p>
<p class="pn-title-2">Bio</p>
<p>Julien Verlaguet is a OCaml programmer with a Master from Université Pierre et Marie Curie in Paris. Before joining Facebook in 2011, he worked at Esterel technologies on verified compilation. At Facebook he designed the Hack programming language, a typed offspring of PHP and managed to convince the majority of developers in the company to add types to their code.</p><p>Brett Simmers is a Software Engineer at Facebook, where he's been working on HHVM for the past five years. He primarily works on the internals of the JIT compiler and HHVM's profile-guided optimizations. Before joining Facebook he spent two years at VMware working on the Linux version of VMware Workstation.</p></div></div><br />
<div id="seminar-54" class="col-md-12 pn-seminar finished"><div id="yee-flix" class="pn-main-informations"><a onclick="return false;" class="pn-title">Implementing a Functional Language for Flix</a>
<br />
<span class="pn-name">Ming-Ho Yee</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://mhyee.com">http://mhyee.com</a>
<br />
<span class="pn-datetime">20 October, 2016 12:00PM <a href="#yee-flix"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Static program analysis is a powerful technique for maintaining software, with applications such as compiler optimizations, code refactoring, and bug finding. Static analyzers are typically implemented in general-purpose programming languages, such as C++ and Java; however, these analyzers are complex and often difficult to understand and maintain. An alternate approach is to use Datalog, a declarative language. Implementors can express analysis constraints declaratively, which makes it easier to understand and ensure correctness of the analysis. Furthermore, the declarative nature of the analysis allows multiple, independent analyses to be easily combined.</p>
<p>Flix is a programming language for static analysis, consisting of a logic language and a functional language. The logic language is inspired by Datalog, but supports user-defined lattices. The functional language allows implementors to write functions, something which is not supported in Datalog. These two extensions, user-defined lattices and functions, allow Flix to support analyses that cannot be expressed by Datalog, such as a constant propagation analysis. Datalog is limited to constraints on relations, and although it can simulate finite lattices, it cannot express lattices over an infinite domain. Finally, another advantage of Flix is that it supports interoperability with existing tools written in general-purpose programming languages.</p>
<p>This talk provides an overview of the implementation and evaluation of the Flix functional language. The implementation involves abstract syntax tree transformations, an interpreter back-end, and a code generator back-end, and must support a number of interesting language features, such as pattern matching, first-class functions, and interoperability. The evaluation compares the interpreter and code generator back-ends in terms of correctness and performance.</p>
<p class="pn-title-2">Bio</p>
<p>Ming-Ho Yee is a Ph.D. student at Northeastern University. He works on programming language design and implementation with Jan Vitek. He received a Bachelor of Software Engineering from the University of Waterloo, and then continued for a Master of Mathematics in Computer Science under the supervision of Ondřej Lhoták.</p></div></div><br />
<div id="seminar-55" class="col-md-12 pn-seminar finished"><div id="wahl-decisions" class="pn-main-informations"><a onclick="return false;" class="pn-title">Behavioral Non-Portability in Decision-Making Programs</a>
<br />
<span class="pn-name">Thomas Wahl</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://www.ccs.neu.edu/home/wahl/">http://www.ccs.neu.edu/home/wahl/</a>
<br />
<span class="pn-datetime">13 October, 2016 12:00PM <a href="#wahl-decisions"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>The precise semantics of floating-point arithmetic programs depends on the execution platform, including the compiler and the target hardware. Such platform dependencies infringe on the highly desirable goal of software portability (which is in fact promised by heterogeneous computing frameworks like OpenCL): the same program run on the same inputs on different platforms can produce different results. In other words, portability does not guarantee reproducibility, and this is a more or less accepted state of affairs.</p>
<p>Serious doubts on the portability of numeric applications arise when differences in results are behavioral, i.e. when they lead to changes in the control flow of a program. In this talk I will first present an algorithm that takes a numeric procedure and determines whether a given input can lead to different decisions depending merely on how the arithmetic in the procedure is compiled and executed. I will then show how this algorithm can be used in static and dynamic analyses of programs, to estimate their numeric stability. I will illustrate the results on examples characteristic of numeric computing where control flow divergence actually occurs across different execution platforms.</p>
<p>Joint with Yijia Gu, Mahsa Bayati, and Miriam Leeser, Northeastern University, Boston, USA</p>
<p class="pn-title-2">Bio</p>
<p>Thomas Wahl joined the faculty of Northeastern University in 2011. His research concerns the reliability (whatever that means) of complex computing systems. Two domains notorious for their fragility are concurrency and numerical computing. With colleagues, Wahl has investigated how floating-point arithmetic can "hijack" a program's computation when run on non-standard architectures, such as heterogeneous and custom-made embedded platforms. You will witness some hijacking attempts in the talk today.</p></div></div><br />
<div id="seminar-56" class="col-md-12 pn-seminar finished"><div id="sen-concolic" class="pn-main-informations"><a onclick="return false;" class="pn-title">Concolic Testing: A Decade Later</a>
<br />
<span class="pn-name">Koushik Sen</span>
<span class="pn-affiliation">University of California, Berkeley</span>
<a class="pn-url" target="_blank" href="https://www.cs.berkeley.edu/~ksen/">https://www.cs.berkeley.edu/~ksen/</a>
<br />
<span class="pn-datetime">6 October, 2016 12:00PM <a href="#sen-concolic"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Symbolic execution, which was introduced more than four decades ago, is typically used in software testing to explore as many different program paths as possible in a given amount of time, and for each path to generate a set of concrete input values exercising it, and check for the presence of various kinds of errors including assertion violations, uncaught exceptions, security vulnerabilities, and memory corruption. A key limitation of classical symbolic execution is that it cannot generate useful test inputs if the program under test uses complex operations such as pointer manipulations and non-linear arithmetic operations.</p>
<p>Our research on Concolic Testing (also known as DART: Directed Automated Random Testing or Dynamic Symbolic Execution) alleviated the limitations of classical symbolic execution by combining concrete execution and symbolic execution. We demonstrated that concolic testing is an effective technique for generating high-coverage test suites and for finding deep errors in complex software applications. The success of concolic testing in scalably and exhaustively testing real-world software was a major milestone in the ad hoc world of software testing and has inspired the development of several industrial and academic automated testing and security tools.</p>
<p>One of the key challenges of concolic testing is the huge number of programs paths in all but the smallest programs, which is usually exponential in the number of static branches in the code. In this talk I will describe MultiSE, a new technique for merging states incrementally during symbolic execution, without using auxiliary variables. The key idea of MultiSE is based on an alternative representation of the state, where we map each variable, including the program counter, to a set of guarded symbolic expressions called a value summary. MultiSE has several advantages over conventional symbolic execution and state merging techniques: 1) value summaries enable sharing of symbolic expressions and path constraints along multiple paths, 2) value-summaries avoid redundant execution, 3) MultiSE does not introduce auxiliary symbolic values, which enables it to make progress even when merging values not supported by the constraint solver, such as floating point or function values. We have implemented MultiSE for JavaScript programs in a publicly available open-source tool. Our evaluation of MultiSE on several programs shows that MultiSE can run significantly faster than traditional symbolic execution.</p>
<p class="pn-title-2">Bio</p>
<p>Koushik Sen is an associate professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. His research interest lies in Software Engineering, Programming Languages, and Formal methods. He is interested in developing software tools and methodologies that improve programmer productivity and software quality. He is best known for his work on ³DART: Directed Automated Random Testing² and concolic testing. He has received a NSF CAREER Award in 2008, a Haifa Verification Conference (HVC) Award in 2009, a IFIP TC2 Manfred Paul Award for Excellence in Software: Theory and Practice in 2010, a Sloan Foundation Fellowship in 2011, a Professor R. Narasimhan Lecture Award in 2014, and an Okawa Foundation Research Grant in 2015. He has won several ACM SIGSOFT Distinguished Paper Awards. He received the C.L. and Jane W-S. Liu Award in 2004, the C. W. Gear Outstanding Graduate Award in 2005, and the David J. Kuck Outstanding Ph.D. Thesis Award in 2007, and a Distinguished Alumni Educator Award in 2014 from the UIUC Department of Computer Science. He holds a B.Tech from Indian Institute of Technology, Kanpur, and M.S. and Ph.D. in CS from University of Illinois at Urbana-Champaign.</p></div></div><br />
<div id="seminar-57" class="col-md-12 pn-seminar finished"><div id="haller-lacasa" class="pn-main-informations"><a onclick="return false;" class="pn-title">LaCasa: Lightweight Affinity and Object Capabilities in Scala</a>
<br />
<span class="pn-name">Philipp Haller</span>
<span class="pn-affiliation">KTH Royal Institute of Technology</span>
<a class="pn-url" target="_blank" href="http://www.csc.kth.se/~phaller/">http://www.csc.kth.se/~phaller/</a>
<br />
<span class="pn-datetime">29 September, 2016 12:30PM <a href="#haller-lacasa"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Aliasing is a known source of challenges in the context of imperative object-oriented languages, which have led to important advances in type systems for aliasing control. However, their large-scale adoption has turned out to be a surprisingly difficult challenge. While new language designs show promise, they do not address the need of aliasing control in existing languages.</p>
<p>This paper presents a new approach to isolation and uniqueness in an existing, widely-used language, Scala. The approach is unique in the way it addresses some of the most important obstacles to the adoption of type system extensions for aliasing control. First, adaptation of existing code requires only a minimal set of annotations. Only a single bit of information is required per class. Surprisingly, the paper shows that this information can be provided by the object-capability discipline, widely-used in program security. We formalize our approach as a type system and prove key soundness theorems. The type system is implemented for the full Scala language, providing, for the first time, a sound integration with Scala’s local type inference. Finally, we empirically evaluate the conformity of existing Scala open-source code on a corpus of over 75,000 LOC.</p>
<p class="pn-title-2">Bio</p>
<p>Philipp Haller is an assistant professor in the theoretical computer science group at KTH Royal Institute of Technology, the leading technical university in Sweden. His main research interests are programming languages, type systems, concurrent, and distributed programming. Philipp is co-author of Scala's async/await extension for asynchronous computations, and one of the lead designers of Scala's futures and promises library. As main author of the book "Actors in Scala," he created Scala's first widely-used actors library. Philipp was co-chair of the 2013 and 2014 editions of the Scala Workshop, and co-chair of the 2015 ACM SIGPLAN Scala Symposium. Previously, he has held positions at Typesafe, Stanford University, and EPFL. He received a PhD in computer science from EPFL in 2010.</p></div></div><br />
<div id="seminar-58" class="col-md-12 pn-seminar finished"><div id="vitek-julia" class="pn-main-informations"><a onclick="return false;" class="pn-title">Performance in Julia</a>
<br />
<span class="pn-name">Jan Vitek</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://janvitek.org/">http://janvitek.org/</a>
<br />
<span class="pn-datetime">15 September, 2016 12:30PM <a href="#vitek-julia"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>Julia, like R, is a dynamic language for scientific computing but, unlike R, it was explicitly designed to deliver performance competitive to traditional batch-compiled languages. To achieve this Julia's designers made a number of unusual choices, including the presence of a set of type annotations that are used for dispatching methods and speed up code, but not for type-checking. The result is that many Julia programs are competitive with equivalent programs written in C. This talk gives a brief overview of the key points of Julia's design and considers whether similar ideas could be adopted in R.</p>
<p class="pn-title-2">Bio</p>
<p>Jan Vitek, <a href=""http://janvitek.org/"">"http://janvitek.org/"</a>, is a Professor at Northeastern University CCIS. He works on the design and implementation of programming abstractions for areas and in languages that are *terrifying*. For instance, he has worked on a real-time JVM for running Java on an actual embedding real-time system, on understanding JavaScript to make it more secure, and on getting R (yes R) to be scalable for data analysis. Apparently he does these things because they are used in the "real world" to "solve problems". He also has an excellent sense of humor and didn't give me a bio, so I took some liberties and hope he doesn't mind.</p></div></div><br />
<div id="seminar-59" class="col-md-12 pn-seminar finished"><div id="zeilberger-refinement" class="pn-main-informations"><a onclick="return false;" class="pn-title">A Categorical Perspective on Type Refinement</a>
<br />
<span class="pn-name">Noam Zeilberger</span>
<span class="pn-affiliation">Inria Ecole Polytechnique</span>
<a class="pn-url" target="_blank" href="http://noamz.org/">http://noamz.org/</a>
<br />
<span class="pn-datetime">13 July, 2016 11:45AM <a href="#zeilberger-refinement"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
<p>A "type refinement system" is a type system built on top of
a typed programming language, as an extra layer of typing. Over the
past few years Paul-André Melliès and I have investigated a
categorical foundation for type refinement systems, which is based on
the idea of looking at a type refinement system "backwards", in terms
of the functor which erases the extra layer of types. The talk will
give an introduction to this framework as well as to some of the
insights that it offers, such as:</p>
<p>* The idea of viewing Hoare logic as a type refinement system</p>
<p>* The importance of the bifibrational operations of "pushing forward" and
"pulling back" (which generalize strongest postconditions and weakest preconditions)</p>
<p>* How those operations can be combined with a monoidal closed structure, to
model type refinement systems built over pure lambda calculus</p>
<p>I will not assume any prior background in category theory, although as background reading audience
members may be interested in the lecture notes for my recent course at OPLSS
(<a href="http://noamz.org/oplss16/refinements-notes.pdf">http://noamz.org/oplss16/refinements-notes.pdf</a>, especially Ch.3).</p>
<p class="pn-title-2">Bio</p>
Since receiving his PhD from Carnegie Mellon in 2009, Noam Zeilberger has been actively pursuing a career as an itinerant postdoc, with gigs in Paris (Laboratoire PPS), Madrid (IMDEA Software), Princeton (IAS), and back in Paris (MSR-Inria). He is currently a member of Inria Team Parsifal at Ecole Polytechnique. In his free time, he enjoys enumerating lambda terms, and his favorite combinators are B, C and I.</div></div><br />
<div id="seminar-60" class="col-md-12 pn-seminar finished"><div id="mickens-dataflow" class="pn-main-informations"><a onclick="return false;" class="pn-title">Leveraging Fine-grained Data Flows in Web Applications</a>
<br />
<span class="pn-name">James Mickens</span>
<span class="pn-affiliation">Harvard University</span>
<a class="pn-url" target="_blank" href="http://mickens.seas.harvard.edu/">http://mickens.seas.harvard.edu/</a>
<br />
<span class="pn-datetime">5 July, 2016 1:30PM <a href="#mickens-dataflow"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
A modern web page contains megabytes of HTML, CSS, images, and JavaScript. Loading such a page requires a browser to evaluate a complex dependency graph involving those resources; once the page is loaded, subsequent interactions between those resources and the user can lead to tricky-to-diagnose bugs. In this talk, I'll describe how tracking fine-grained data flows can allow us to reduce page load times by prioritizing the loads of the highest ancestors in the data flow graph. I'll also describe initial work in using data flows to assist with time-travel debugging (in which developers use a logging-and-replay framework to analyze buggy program executions).
<p class="pn-title-2">Bio</p>
James Mickens is an IEEE Knight of the Republic, an ACM Templar for Non-Open Access, and a Royal Proceeding of Her Majesty’s Royal Proceedings. His appreciation for syntactically correct code has led him to be called “a semicolon in human form.” His online shopping habits have too many dimensions to be k-means clustered, so he is only shown ads about dinosaurs and ancient siege machines. This does not bother James Mickens, and explains why he spends his summers attacking France with triceratops horns.</div></div><br />
<div id="seminar-61" class="col-md-12 pn-seminar finished"><div id="scherer-effects" class="pn-main-informations"><a onclick="return false;" class="pn-title">New language ideas for user-defined side-effects: algebraic effect handlers.</a>
<br />
<span class="pn-name">Gabriel Scherer</span>
<span class="pn-affiliation">Northeastern University</span>
<a class="pn-url" target="_blank" href="http://gallium.inria.fr/~scherer/">http://gallium.inria.fr/~scherer/</a>
<br />
<span class="pn-datetime">18 May, 2016 11:45AM <a href="#scherer-effects"><span class="glyphicon glyphicon-link"></span></a></span>
<span class="pn-room">WVH 366</span>
<span class="pn-room"></span></div>
<div class="pn-abstract-bio"><p class="pn-title-2">Abstract</p>
This talk reports on some cool ideas I learned during a week-long
seminar in Dagstuhl last month; it will present other people's work,
not my own. It is aimed at an audience interested in programming
language design in general, but not familiar with the theoretical
treatment of pure languages and side-effects.
We shall start with *demos* first, explaining short code examples in
three programming languages: ML with exceptions as a warmup, then the
new language 'Eff' of Matija Pretnar and Andrej Bauer, that first
implemented so-called effect handlers, and finally the language
'Frank' of Conor McBride, that integrates these handlers in a more
uniform style of "effectful call-by-value programming".
Only second will we discuss some *theory*, in an accessible way:
monads and algebraic effects, which are two distinct ways to formalize
side-effects, and the difference between "direct" and "indirect" style
of effectful programming.