The 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 (2020). 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 CEST) and will be streamed live on YouTube, where edited videos will also be posted after the event. Questions will be taken through sli.do (where we prefer you to sign in with your full name, so the speaker sees who is asking each question).
Google Calendar Link (iCal)
upcoming talks
past talks
2020-05-11
"A quick look at impredicativity"
by Simon Peyton Jones (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.
#researchSeminar video on Youtube
"A quick look at impredicativity"
by Simon Peyton Jones (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.
#researchSeminar video on Youtube
2020-05-18
"Backtracking Generators for Random Testing"
by Benjamin Pierce (UPenn) Host: John Hughes
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.
#researchSeminar video on Youtube
"Backtracking Generators for Random Testing"
by Benjamin Pierce (UPenn) Host: John Hughes
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.
#researchSeminar video on Youtube
2020-05-25
"Liquid resource types for verification and synthesis"
by Nadia Polikarpova (UCSD) Host: Koen Claessen
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 of Computer Science and Engineering at the University of California, San Diego. She is a 2020 Sloan Fellow and a recipient of the 2020 NSF Career Award. Her research interests are in program synthesis, program verification, and type systems.
audience: The talk should be accessible to anyone comfortable with statically-typed functional languages; familiarity with expressive type systems (refinement types, dependent types) will be helpful, but is not required.
#researchSeminar video on Youtube (slides)
"Liquid resource types for verification and synthesis"
by Nadia Polikarpova (UCSD) Host: Koen Claessen
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 of Computer Science and Engineering at the University of California, San Diego. She is a 2020 Sloan Fellow and a recipient of the 2020 NSF Career Award. Her research interests are in program synthesis, program verification, and type systems.
audience: The talk should be accessible to anyone comfortable with statically-typed functional languages; familiarity with expressive type systems (refinement types, dependent types) will be helpful, but is not required.
#researchSeminar video on Youtube (slides)
2020-06-01
"Using Formal Methods to Eliminate Exploitable Bugs"
by Kathleen Fisher (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.
Professor Kathleen Fisher is Chair of the Department of Computer Science at Tufts University. Previously, she was a Program Manager at DARPA and a Principal Member of the Technical Staff at AT&T Labs Research. She received her PhD in Computer Science from Stanford University. Kathleen is a Fellow of the Association of Computing Machinery (ACM) and a Hertz Foundation Fellow. Service to the community has been a hallmark of Kathleen's career. She served as Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN) and as Program Chair for three of SIGPLAN's marquee conferences. She is Chair of DARPA's ISAT Study Group and a member of the Board of Trustees of Harvey Mudd College. Kathleen has long been a leader in the effort to increase diversity and inclusion in Computer Science: she was Co-Chair of the Computing Research Association's Committee on the Status of Women (CRA-W) for three years, and she co-founded SIGPLAN's Programming Language Mentoring Workshop (PLMW) Series. Kathleen is a recipient of the SIGPLAN Distinguished Service Award.
Kathleen's research focuses on advancing the theory and practice of programming languages. All of her work is collaborative and much is interdisciplinary. Three main thrusts of her work are (1) designing domain-specific languages to make it easier to write programs in particular domains, (2) developing program synthesis techniques, which use search to generate programs from high-level specifications, and (3) applying principled techniques to produce software that is provably functionally correct with the goal of making hacking much harder.
#research #applicationSeminar video on Youtube
"Using Formal Methods to Eliminate Exploitable Bugs"
by Kathleen Fisher (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.
Professor Kathleen Fisher is Chair of the Department of Computer Science at Tufts University. Previously, she was a Program Manager at DARPA and a Principal Member of the Technical Staff at AT&T Labs Research. She received her PhD in Computer Science from Stanford University. Kathleen is a Fellow of the Association of Computing Machinery (ACM) and a Hertz Foundation Fellow. Service to the community has been a hallmark of Kathleen's career. She served as Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN) and as Program Chair for three of SIGPLAN's marquee conferences. She is Chair of DARPA's ISAT Study Group and a member of the Board of Trustees of Harvey Mudd College. Kathleen has long been a leader in the effort to increase diversity and inclusion in Computer Science: she was Co-Chair of the Computing Research Association's Committee on the Status of Women (CRA-W) for three years, and she co-founded SIGPLAN's Programming Language Mentoring Workshop (PLMW) Series. Kathleen is a recipient of the SIGPLAN Distinguished Service Award.
Kathleen's research focuses on advancing the theory and practice of programming languages. All of her work is collaborative and much is interdisciplinary. Three main thrusts of her work are (1) designing domain-specific languages to make it easier to write programs in particular domains, (2) developing program synthesis techniques, which use search to generate programs from high-level specifications, and (3) applying principled techniques to produce software that is provably functionally correct with the goal of making hacking much harder.
#research #applicationSeminar video on Youtube
2020-06-08
"Featherweight Go"
by Phil Wadler (University of Edinburgh) Host: Koen Claessen
We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structural, and whereas generics in Java are defined via erasure, in Go we use monomorphisation. Although monomorphisation is used widely, we are one of the first to formalise it. Our design also supports a solution to The Expression Problem.
#research #work-in-progressSeminar video on Youtube (slides)
"Featherweight Go"
by Phil Wadler (University of Edinburgh) Host: Koen Claessen
We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structural, and whereas generics in Java are defined via erasure, in Go we use monomorphisation. Although monomorphisation is used widely, we are one of the first to formalise it. Our design also supports a solution to The Expression Problem.
Joint work with: Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance Taylor, Bernardo Toninho, and Nobuko Yoshida.
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: Anyone interested in programming languages. Mostly Go code, with a little formalisation.
#research #work-in-progressSeminar video on Youtube (slides)
2020-06-15
"Concolic Testing with Higher-Order Inputs"
by Robby Findler (Northwestern University) Host: John Hughes
Concolic testing, dating back to the mid 2000s, has proven to be an effective, automatic testing technique. Roughly, a concolic tester monitors the program's behavior, collecting information that connects the branches that the program takes with the original inputs to the program. It then uses that information (with the help of an SMT solver) to try to construct new inputs to force the program to take different branches, in an attempt to uncover problems with the program.
Most of the existing work on concolic testing focuses on the situation where the inputs to the program being tested are flat values (e.g., numbers) instead of higher-order values (e.g., objects or functions). Higher-order inputs, however, present challenges for concolic testing because the interplay between the input and the program being tested is much more complex.
In this talk, I'll discuss the way we generalize concolic testing to higher-order inputs, explaining why it is challenging and how we answer the challenge. The talk will be example driven and I will try to bring across the intuition for how we conceptualize the generalization to higher-order inputs and the results we have so far.
(Joint work with Shu-Hung You and Christos Dimoulas.)
Robby Findler is a core developer of Racket and a professor at Northwestern University.
audience: People interested in functional programming research. Familiarity with concolic testing is not assumed but being able to read small fragments of code (possibly with lambdas in them) is.
#research #work-in-progress #funky-functionsSeminar video on Youtube (slides)
"Concolic Testing with Higher-Order Inputs"
by Robby Findler (Northwestern University) Host: John Hughes
Concolic testing, dating back to the mid 2000s, has proven to be an effective, automatic testing technique. Roughly, a concolic tester monitors the program's behavior, collecting information that connects the branches that the program takes with the original inputs to the program. It then uses that information (with the help of an SMT solver) to try to construct new inputs to force the program to take different branches, in an attempt to uncover problems with the program.
Most of the existing work on concolic testing focuses on the situation where the inputs to the program being tested are flat values (e.g., numbers) instead of higher-order values (e.g., objects or functions). Higher-order inputs, however, present challenges for concolic testing because the interplay between the input and the program being tested is much more complex.
In this talk, I'll discuss the way we generalize concolic testing to higher-order inputs, explaining why it is challenging and how we answer the challenge. The talk will be example driven and I will try to bring across the intuition for how we conceptualize the generalization to higher-order inputs and the results we have so far.
(Joint work with Shu-Hung You and Christos Dimoulas.)
Robby Findler is a core developer of Racket and a professor at Northwestern University.
audience: People interested in functional programming research. Familiarity with concolic testing is not assumed but being able to read small fragments of code (possibly with lambdas in them) is.
#research #work-in-progress #funky-functionsSeminar video on Youtube (slides)
2020-06-22
"Strongly Typed System F in GHC"
by Stephanie Weirich (UPenn) Host: Koen Claessen
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.
Stephanie Weirich is the ENIAC President's Distinguished Professor of Computer and Information Science at the University of Pennsylvania. Her research interests include statically-typed functional programming, dependent types, interactive theorem proving and programming language theory. She is the General Chair of ICFP 2020 and hopes to see you (virtually) in August.
audience: Haskellers that are familiar with GADTs and/or strongly typed abstract syntax.
#research #tutorialMonday 2020-06-22, 7am PDT / 10am EDT / 16:00 CEST (YouTube) (Sli.do, event code #4687)
"Strongly Typed System F in GHC"
by Stephanie Weirich (UPenn) Host: Koen Claessen
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.
Stephanie Weirich is the ENIAC President's Distinguished Professor of Computer and Information Science at the University of Pennsylvania. Her research interests include statically-typed functional programming, dependent types, interactive theorem proving and programming language theory. She is the General Chair of ICFP 2020 and hopes to see you (virtually) in August.
audience: Haskellers that are familiar with GADTs and/or strongly typed abstract syntax.
#research #tutorialMonday 2020-06-22, 7am PDT / 10am EDT / 16:00 CEST (YouTube) (Sli.do, event code #4687)
2020-06-29
"Algorithm Design with Haskell"
by Jeremy Gibbons (Oxford University) Host: Mary Sheeran
The talk is related to our new book: "Algorithm Design with Haskell" 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 #programmingSeminar video on Youtube (slides)
"Algorithm Design with Haskell"
by Jeremy Gibbons (Oxford University) Host: Mary Sheeran
The talk is related to our new book: "Algorithm Design with Haskell" 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 #programmingSeminar video on Youtube (slides)