he Chalmers Online Functional Programming Seminar Series is organized by the Chalmers Functional Programming Group, as a way to exploit the fact that so many of us in the FP community are already meeting and working online these days. Our aim is to bring the people in the FP community closer together, to educate and inspire, and to foster collaboration. The seminars will take place every Monday (at 7am PDT / 10am EDT / 16:00 CET) and are organized through Zoom. Google Calendar Link
upcoming talks
May 11
"A quick look at impredicativity"
by
(Microsoft Research) Host: John Hughes
Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. I’ve been trying to fix this flaw for over 15 years , but every time I ended up with a system that was unusably complicated.
But now I think we have it! Quick Look is a practical, implemented, and deployable design for impredicative type inference. It is simple to explain (although you can be the judge of that), and crucially it can be implemented with modest, localised changes that are fully compatible with GHC’s myriad other type system extensions.
Simon Peyton Jones, FRS, graduated from Trinity College Cambridge in 1980. After two years in industry, he spent seven years as a lecturer at University College London, and nine years as a professor at Glasgow University, before moving to Microsoft Research (Cambridge) in 1998. Simon’s main research interest is in functional programming languages, their implementation, and their application. He was a key contributor to the design of the now-standard functional language Haskell, and is the lead designer of the widely-used Glasgow Haskell Compiler (GHC). He has written two textbooks about the implementation of functional languages. He is particularly motivated by direct application of principled theory to practical language design and implementation — that is one reason he loves functional programming so much. Simon is chair of Computing at School, the grass-roots organisation that was at the epicentre of the 2014 reform of the English computing curriculum.
audience: Anyone interested in statically-typed functional programming.
#research
May 18
"Backtracking Generators for Random Testing"
by
(UPenn) Host: Koen Claessen
QuickCheck-style property-based testing relies on random generators that produce well-distributed test data. When the properties under test involve sparse preconditions, test generators must be written so as to produce constrained test data satisfying these preconditions. But what should such generators do when choices made early on render later constraints unsatisfiable? How can generation effort be reused, both when failure is a possibility and, more generally, when parts of a complex test are relatively expensive to generate? The natural answer to all these questions is to use backtracking.
We propose a new generator abstraction, extending QuickCheck generators with local backtracking by enriching the key Gen monad to support backtracking under the hood; and we show, in this setting, how local backtracking can significantly improve end-to-end bug-finding performance in two case studies. We show, first, that adding a small amount of backtracking improves the performance of a generator for well-typed System F terms by 1.6× on average. When generating System F terms, backtracking allows us to avoid completely discarding generation effort in the presence of uninhabitable types, which we find allows us to produce larger, more effective test cases—requiring 2.1× fewer tests, on average, to discover a bug. Second, we show that adding backtracking to an existing, highly tuned generator for random machine states in a testing framework for dynamic information flow control monitors allows us to amortize an expensive step in test-case generation, improving bug-finding performance by 3.9× with only a tiny change in the generator.
Benjamin Pierce is Henry Salvatori Professor of Computer and Information Science at the University of Pennsylvania and a Fellow of the ACM. His research interests include programming languages, type systems, language-based security, computer-assisted formal verification, differential privacy, and synchronization technologies. He is the author of the widely used graduate textbooks Types and Programming Languages and Software Foundations. He has served as co-Editor in Chief of the Journal of Functional Programming, as Managing Editor for Logical Methods in Computer Science, and as editorial board member of Mathematical Structures in Computer Science, Formal Aspects of Computing, and ACM Transactions on Programming Languages and Systems. He holds a doctorate honoris causa from Chalmers University. He is also the lead designer of the popular Unison file synchronizer.
audience: Anyone interested in property-based testing.
#research
May 25
"Liquid resource types for verification and synthesis"
by
(UCSD) Host: John Hughes
This talk presents a type system that combines Liquid Types with potential annotations from Automated Amortized Resource Analysis to enable fine-grained reasoning about resource consumption. Using Liquid Resource Types we can verify, for example, that insertion sort only makes as many steps as there are unordered pairs in its input list. We can also use these types in conjunctions with type-driven program synthesis to synthesize provably efficient programs.
Nadia Polikarpova is an Assistant Professor in the Computer Science and Engineering Department at the University of California, San Diego. She completed her PhD in 2014 at ETH Zurich (Switzerland) under the supervision of Bertrand Meyer. After that, she spent almost three years as a postdoc at MIT CSAIL, working with Armando Solar-Lezama. Her research interests span the areas of programming languages and formal methods; in particular, she is interested in building practical tools and techniques that make it easier for programmers to construct secure and reliable software.
#research
June 1
"Using Formal Methods to Eliminate Exploitable Bugs"
by
(Tufts University, Former Program Manager of DARPA’s HACMS Program) Host: Mary Sheeran
For decades, formal methods have offered the promise of software that doesn’t have exploitable bugs. Until recently, however, it hasn’t been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. It has been proven to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and to enforce integrity and confidentiality properties. The CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution in the formal methods community, including increased processor speed, better infrastructure like the Isabelle/HOL and Coq theorem provers, specialized logics for reasoning about low-level code, increasing levels of automation afforded by tactic languages and SAT/SMT solvers, and the decision to move away from trying to verify existing artifacts and instead focus on co-developing the code and the correctness proof. In this talk I will explore the promise and limitations of current formal methods techniques for producing useful software that provably does not contain exploitable bugs. I will discuss these issues in the context of DARPA’s HACMS program, which had as its goal the creation of high-assurance software for vehicles, including quad-copters, helicopters, and automobiles.
#research #application
June 8
"Featherweight Go"
by
(University of Edinburgh) Host: Koen Claessen
The Go programming language was released by Google a decade ago, and recently its authors have considered how to extend it with generic types. This talk describes a design for generics in Go founded in the principles of programming languages, inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. We begin by presenting Featherweight Go (FG), a simplified version of the Go language, and Featherweight Generic Go (FGG), an extension of FG to support generic types. For each we show standard preservation and progress results. Finally, we show that FGG can be translated into FG by a process known as \emph{monomorphisation}, and show that the translation preserves typing and operational semantics.
Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK. He is an ACM Fellow, a Fellow of the Royal Society of Edinburgh, and editor-in-chief of Proceedings of the ACM for Programming Languages. He is past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, winner of the SIGPLAN Distinguished Service Award, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of over 70 with more than 25,000 citations to his work, according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004), Generics and Collections in Java (O'Reilly, 2006), and Programming Language Foundations in Agda (2018). He has delivered invited talks in locations ranging from Aizu to Zurich.
audience: Researchers
#research #work-in-progress
June 15
"Higher-order concolic testing"
by
(Northwestern University) Host: Koen Claessen
I will explain what higher-order concolic testing is (using concolic testing on programs that accept functions as inputs). I will try to be very example-driven to explain what we've figured out about the problem so far.
audience: People need to be used to reading short fragments of code with lambdas in them
#research #work-in-progress
June 22
"Strongly Typed System F in GHC"
by
(UPenn) Host: Mary Sheeran
There are many examples that demonstrate how to create a strongly typed abstract syntax in Haskell for a language with a simple type system. But there are many fewer examples that allow the embedded language to be polymorphic. I will work through what it takes to do so, touching on variable binding representations, and exploring the limits of dependently-typed programming in GHC.
audience: Haskellers that are familiar with GADTs and/or strongly typed abstract syntax.
#research
June 29
"Algorithm Design with Haskell"
by
(Oxford University) Host: Koen Claessen
The talk is related to our new book: "
" by Richard Bird and Jeremy Gibbons.
The book is devoted to five main principles of algorithm design: divide and conquer, greedy algorithms, thinning, dynamic programming, and exhaustive search. These principles are presented using Haskell, leading to simpler explanations and shorter programs than would be obtained with imperative languages. Carefully selected examples, both new and standard, reveal the commonalities and highlight the differences between algorithms. The algorithm developments use equational reasoning where applicable, clarifying the applicability conditions and correctness arguments. In the talk, I propose to describe the premise of the book, including in particular the small aspect in which Haskell is insufficient, and to give an example.
I am a Professor of Computing in the Department of Computer Science at the University of Oxford. I am currently Director of the Software Engineering Programme, which offers part-time professional Masters’ degrees in Software Engineering and in Software and Systems Security. I also lead the Algebra of Programming research group. I am Editor-in-Chief of the Journal of Functional Programming, Past Vice Chair of ACM SIGPLAN, Past Chair of IFIP WG2.1. Before taking up this post in 1999, I held lectureships at Oxford Brookes University and the University of Auckland, New Zealand.
audience: Students (both undergraduate and postgraduate), researchers, teachers, and professionals who want to know more about what goes into a good algorithm and how such algorithms can be expressed in purely functional terms.
#research #pearl #tutorial #applications #programming