Lambda Days 2021

This video was recorded at a pre-conference meet-up of Lambda Days, which took place on 4th February 2021 - https://www.lambdadays.org/lambdadays2021/#free-meetup More great virtual tech conferences - https://codesync.global --- Dependent Types - salvation or plague run by John Hughes with Stephanie Weirich, Edwin Brady, Adam Chlipala and Thorsten Altenkirch introduced by Michał Ślaski ABSTRACT Does the future belong to dependent types… or not? Are they a cute toy, or the Next Big Thing? Should you be planning to use them in your next project (or the next but ten), and if so, where and how should you start? What are the swings and roundabouts you should be aware of? Our panelists are leading the adoption of dependent types in a variety of programming languages, and have deep insights into how they scale in practice. Join us to learn if dependent types will be a part of your future! Need a refresher? We’ll be starting at the beginning, but we will be going fast—if you’d like to prepare a little in advance, I recommend watching Thorsten Altenkirch’s video “The power of Π” (from last year’s Lambda Days): https://www.youtube.com/watch?v=3zT5eVHpQwA --- THE HOST - John Hughes John Hughes has been a functional programming enthusiast for more than thirty years, at the Universities of Oxford, Glasgow, and since 1992 Chalmers University in Gothenburg, Sweden. He served on the Haskell design committee, co-chairing the committee for Haskell 98, and is the author of more than 100 papers, including "Why Functional Programming Matters", one of the classics of the area. With Koen Claessen, he created QuickCheck, the most popular testing tool among Haskell programmers, and in 2006 he founded Quviq to commercialise the technology using Erlang. In 2018 he became an ACM Fellow. THE PANELISTS Adam Chlipala - Associate Professor of Computer Science, MIT Computer Science & Artificial Intelligence Lab Edwin Brady - Creator of the Idris programming language, University of St Andrews Niki Vazou - Research Assistant Professor, IMDEA Stephanie Weirich - Professor of Computer Science, University of Pennsylvania Thorsten Altenkirch - Professor of Computer Science, University of Nottingham --- Lambda Days Website: https://www.lambdadays.org Twitter: https://twitter.com/LambdaDays

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021/#free-meetup More great virtual tech conferences - https://codesync.global --- Introducing Nx by José Valim ABSTRACT In this presentation, José Valim will introduce the Nx project, which brings numerical computing to Elixir. José Valim will explore topics such as multi-dimensional tensors, automatic differentiation, as well as JIT compilation to the CPU/GPU. --- SPEAKER - José Valim Creator of Elixir, Chief Adoption Officer @ Dashbit José Valim is the creator of the Elixir programming language. He graduated in Engineering in São Paulo University, Brazil and has a Master of Science by Politecnico di Torino, Italy. He runs Dashbit alongside a team of Elixir experts to help companies and startups adopt and run Elixir in production. --- Lambda Days Website: https://www.lambdadays.org Twitter: https://twitter.com/LambdaDays

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 Industry versus academia? Learning and teaching programming by Francesco Cesarini & Simon Thompson ABSTRACT In our talk we’ll explore this hypothesis: in industry, you are learning a technology you will use to develop software, whereas in an academic setting, you are there to learn how to learn. Based on our experience of travelling in opposite directions: Francesco from industry to academia, and Simon from a theoretical to a more pragmatic approach, we’ll test the hypothesis, and, through evidence and anecdotes, show that in fact it is more complicated and diverse than we had first imagined. • Follow us on social: Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​ • Looking for a unique learning experience? Attend the next Code Sync conference near you! See what's coming up at: https://codesync.global • SUBSCRIBE TO OUR CHANNEL https://www.youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Keynote: Functorio - having fun with functional programming by Bartosz Milewski ABSTRACT If you didn't know about functional programming, you could have discovered it yourself... playing the game called Factorio. I was fascinated by this world-building game and discovered that it inadvertently illustrated a lot of functional programming ideas. I was immediately able to identify functions, function objects, and functors. Then I started speculating about what features I would add to the game to implement applicatives, monads, algebras, etc. I want to share the fun of discovery with you. --- SPEAKER - Bartosz Milewski BartoszMilewski.com Bartosz started as a quantum physicist, joined Microsoft to build the search engine for Windows and became an avid proponent of OOP. Then he got into concurrency and parallelism and now he’s evangelizing FP. He is an author of a book Category Theory for Programmers. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Keynote: Excel meets Lambda by Andy Gordon, Simon Peyton Jones ABSTRACT The world’s most widely used programming language is a purely functional language! It’s called Excel. No mutable cells, assignment statements, or sequencing; just pure functions and immutable values. But, despite its phenomenal success, considered as a functional programming language, Excel’s formulas constitute a very limited language: it is largely restricted to scalar values, and you can’t write new user-defined functions. Until now. Excel has just released LAMBDA, in its full higher-order glory, just as Alonzo Church defined it in the 1930s. That’s pretty exciting, because now you can define new functions, which can call other lambda-defined functions, to arbitrary depth, and even recursively. It represents a qualitative change not an incremental one: Excel just became Turing-complete. In this talk we’ll tell you some things you may not know about Excel’s existing formula language, we’ll describe the journey that led a few geeks at Microsoft Research Cambridge to influence one of the most widely used programs in history, and we’ll show you some other ideas we’ve been playing around with. Lambda Days indeed! --- SPEAKER - Andy Gordon Head of Calc Intelligence, Microsoft Research Andy’s research is on programming languages: their principles, logic, usability, and trustworthiness. His work has had impact on several best-in-class programming languages, including refinement types for security in F*. Today, he leads the Calc Intelligence team doing research on end-user programming, especially in spreadsheets. As a research manager, Andy strives for a diverse and inclusive team. He and his team collaborate closely with the Excel product group. Features such as LAMBDA and Calc.ts, arising from their mission to enhance Excel as a programming language, ship now in production to millions of customers. SPEAKER - Simon Peyton Jones Lead designer of the Glasgow Haskell Compiler, Principal researcher at Microsoft Research Simon has been a researcher at Microsoft Research in Cambridge, England since Sept 1998. He's also an Honorary Professor of the Computing Science Department at Glasgow University, where he was a professor during 1990-1998. Simon is interested in the design, implementation, and application of lazy functional languages. In practical terms, that means he spends most of his time on the design and implementation of the language Haskell. In particular, much of his work is focused around the Glasgow Haskell Compiler, and its ramifications. Simon is chair of Computing at School, the group at the epicentre of the reform of the national curriculum for Computing in England. Computer science is now a foundational subject, alongside maths and natural science, that every child learns from primary school onwards (background here). --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Hardware as Software by Pat Hanrahan ABSTRACT We are entering a new era of computer architecture. Due to the end of Moore's Law and Dennard Scaling, the best way to build more efficient computers is to use domain-specific specialized architectures. Many systems companies such as Amazon, Apple, Google, and Facebook now have active hardware efforts. Unfortunately, building hardware is very difficult compared to software. But hardware is just software! In this talk I will talk about how to use functional programming to describe hardware. Thinking of hardware as software leads to better ways of building hardware. Thinking of software as hardware, leads to better way to program in general. --- SPEAKER - Pat Hanrahan Professor of Computer Science and Electrical Engineering in the Computer Graphics Laboratory at Stanford University Pat Hanrahan is the CANON Professor of Computer Science and Electrical Engineering at Stanford University where he teaches computer graphics. His current research involves graphics systems and architectures, hardware design tools, programming languages, image synthesis, and visualization. Early in his career, Pat worked at Pixar where he developed software for volume rendering and was the chief architect of the RenderMan(TM) Interface - a protocol that allows modeling programs to describe scenes to high quality rendering programs. In addition to being an early employee at PIXAR, he has founded three companies, PeakStream, BeBop, and Tableau, and has served on the technical advisory boards of NVIDIA, Exluna, Neoptica, VSee, Procedural, and SkyTree. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Keynote: (Programming Languages) in Agda = Programming (Languages in Agda) by Philip Wadler ABSTRACT The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by recursion. Dependently-typed programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program. This talk introduces Programming Language Foundations in Agda, a new textbook that is also an executable Agda script---and also explains the role Agda is playing in IOHK's new cryptocurrency. The textbook is freely available at plfa.inf.ed.ac.uk. --- SPEAKER - Philip Wadler Co-creator of Haskell, Professor of Theoretical Computer Science at University of Edinburgh Philip Wadler likes to introduce theory into practice, and practice into theory. An example of theory into practice: GJ, the basis for Java with generics, derives from quantifiers in second-order logic. An example of practice into theory: Featherweight Java specifies the core of Java in less than one page of rules. He is a principal designer of the Haskell programming language, contributing to its two main innovations, type classes and monads. The YouTube video of his Strange Loop talk Propositions as Types has over 75,000 views. 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. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Constructive Bidirectional Programming by Zhenjiang Hu ABSTRACT Bidirectional Transformation provides a powerful mechanism for synchronizing and maintaining the consistency of information between different representations. Although many languages have been proposed to support programming bidirectional transformations, we are lacking systematic ways to develop both correct and efficient bidirectional transformation. In this talk, we show that the program calculation technique, which is known to be useful for development of unidirectional functional programs, is useful for systematic development of correct and efficient bidirectional functional programs from a straightforward specification through correctness-preserving calculation. --- SPEAKER - Zhenjiang Hu Head of Department of Computer Science and Technology @ Peking University Zhenjiang Hu is a chair professor and the head of Department of Computer Science and Technology, Deputy Dean of School of Electronics Engineering and Computer Science, Peking University. His main interest is in programming languages and software engineering in general, and functional programming, bidirectional transformation, and parallel programming in particular. His work is characterized by developing methodologies to support rigorous development of robust software systems. He was awarded the basic research achievement awards from Japan Society for Software Science and Technology. He is famous for his contribution to the establishment of the well-known NII Shonan Meetings. He is Fellow of Japan Federation of Engineering Society, ACM Distinguished Scientist, Member of European Academy of Sciences, IEEE Fellow, Member of Engineering Academy of Japan. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

Promo video of Lambda Days 2021

This video was recorded at the virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays... More great virtual tech conferences - https://codesync.global​ --- Sound on BEAM Music in the Land of Distributed Lisp by Duncan McGreggor ABSTRACT While not built for sound or digital signal processing, Erlang excels in the realm where music control systems have converged: network message-passing. In this talk, Duncan will provide some background on the functional nature of electronics used in music, with a special focus on analog synthesis a la Moog modular systems. Previous sound-generation work on the BEAM will be covered before diving into a new effort along similar lines being made in Lisp Flavoured Erlang (LFE). Practical issues with integrating multiple well-established improvisational tools and music recording systems with a functional programming language will be covered. In addition, LFE's strength as a platform for creating DSL's will be discussed in the dual context of integrating systems and creating generative music. --- SPEAKER - Duncan McGreggor Duncan started hacking in the early 80s on copies of the BSD games, was a linguist in the 101st Airborne Division, studied physics and applied maths at university, traveled to India to practice meditation and dialectic with monks in exile, and eventually joined a startup just before the Internet crash in 1999/2000. Somehow, that did not deter his life-long passion for programming: he started hacking on small, distributed services in the early 2000s, eventually became a Fellow at the Python Software Foundation, joined Robert Virding as a contributor to LFE, and coded in another Lisp for the USGS (LANDSAT data) and then NASA. Duncan is currently a principal engineer at MediaMath, dedicated to building better engineering teams and software engineering practices while also teaching new generations of engineers a love for the art. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at Lambda Days Virtual 2021 - https://www.lambdadays.org/lambdadays2021 Multicloud bindings from web pages | Michał J. Gajda, Science-based solutions ABSTRACT We address a practical problem of inter-language interoperability with cloud APIs from different vendors with HTML documentation and REST calling conventions. We solve this problem, by providing implementing a retargetable cloud application programming interface (API) binding generator. The code for the proposed API is implemented in Haskell, utilising type classes, types a la carte, and a code generation monad (design pattern). It also targets Haskell and allows binding cloud APIs on a short notice and an unprecedented scale. We also note that it significantly decreases maintenance issues with large cloud API bindings due to decreased code-base. • Follow us on social: Twitter: https://twitter.com/LambdaDays LinkedIn: ttps://www.linkedin.com/company/lambda-days • Looking for a unique learning experience? Attend the next Lambda Days conference! See what's coming up at: https://www.lambdadays.org • SUBSCRIBE TO OUR CHANNEL https://www.youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw

This video was recorded at Lambda Days Virtual 2021 - https://www.lambdadays.org/lambdadays2021 Dynamic Creation of Well Typed DSL Expressions | Pieter Koopman ABSTRACT Interactive systems can require complex input from their users. A grammar specifies the allowed expressions in such a Domain Specific Language, DSL. An algebraic DataType, ADT, is a direct representation of such a grammar. For most end-users a structured editor with pull-down menus is much easier to use than a free text editor. The iTask system can derive such structured editors based on an ADT using datatype generic programming. However, the input DSL has often also semantic constraints, like proper use of types and variables. A solution is to use a shallow embedded DSL or a DSL based on a Generalized ADT to specify the input. However, such a specification cannot be handled by datatype generic programming. Hence, one cannot derive structured editors for such a DSL. As a solution, we introduce structured web-editors that are based on dynamic types. These dynamic types are more expressive; they can express the required DSL constraints. In the new dynamic editor library we need to specify just the dynamic relevant for the DSL. The library takes care of displaying the applicable instances to the user and calls itself recursively to create the arguments of the dynamic functions. In this paper we show how this can be used to enforce the requires constraints on ADTs, to create structured web-editors for shallow embedded DSLS, and to create those editors for GADT based DSLs. • Follow us on social: Twitter: https://twitter.com/LambdaDays LinkedIn: ttps://www.linkedin.com/company/lambda-days • Looking for a unique learning experience? Attend the next Lambda Days conference! See what's coming up at: https://www.lambdadays.org • SUBSCRIBE TO OUR CHANNEL https://www.youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw

This video was recorded at Lambda Days Virtual 2021 - https://www.lambdadays.org/lambdadays2021 Fast XML HTML for Haskell XML TypeLift | Michał J. Gajda, Science-based solutions ABSTRACT We presents and compares a range of parsers with and without data mapping for conversion between XML and Haskell. The best performing parser competes favorably with the fastest tools available in other languages and is, thus, suitable for use in large-scale data analysis. The best performing parser also allows software developers of intermediate-level Haskell programming skills to start processing large numbers of XML documents soon after finding the relevant XML Schema from a simple internet search, without the need for specialist prior knowledge or skills. We hope that this unique combination of parser performance and usability will provide a new standard for XML mapping to high-level languages. • Follow us on social: Twitter: https://twitter.com/LambdaDays LinkedIn: ttps://www.linkedin.com/company/lambda-days • Looking for a unique learning experience? Attend the next Lambda Days conference! See what's coming up at: https://www.lambdadays.org • SUBSCRIBE TO OUR CHANNEL https://www.youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw

This video was recorded at Lambda Days Virtual 2021 - https://www.lambdadays.org/lambdadays2021 Building Full Stack Web Applications with Safe Stack | Ody Mbegbu ABSTRACT As the web has become more and more ubiquitous and people are now doing even more online. Web Development has only grown in complexity from it's humble days of serving documents. Today, Modern Web Applications are quite complex. And if you don't want to build it in Javascript, you typically have to use two languages, One for the front end and the other for the backend. SAFE Stack provides an alternative allowing you to build the entire application in F# with superb type safety and still keep the flexibility of a scripting language like Python. In my talk, I will show you how to get started building a web application using Safe Stack. • Follow us on social: Twitter: https://twitter.com/LambdaDays LinkedIn: ttps://www.linkedin.com/company/lambda-days • Looking for a unique learning experience? Attend the next Lambda Days conference! See what's coming up at: https://www.lambdadays.org • SUBSCRIBE TO OUR CHANNEL https://www.youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 Secrets of type driven program synthesis by Edwin Brady ABSTRACT Idris is a functional programming language with first-class types, where types may be parameterised by other values. This gives the language implementation a lot of information up front about what a function should do, which means we can use Idris is our interactive assistant, where we write programs by conversation with the machine. As part of this, we are actively developing program synthesis tools, which generate fragments of programs from types. This can appear like magic! However, the key ideas are surprisingly simple. In this talk, I will demonstrate the current state of program synthesis and Idris, and try to demystify how it works, as well as discuss some related work and possible future research directions. • Follow us on social: Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​ • Looking for a unique learning experience? Attend the next Code Sync conference near you! See what's coming up at: https://codesync.global • SUBSCRIBE TO OUR CHANNEL https://www.youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw SPEAKER - Edwin Brady Creator of the Idris programming language Edwin is Lecturer in Computer Science at the University of St Andrews in Scotland, interested in type-driven development, domain-specific languages and reasoning about effectful programs. When he's not doing that, he might be playing Go, watching cricket, or wandering around Scotland's hills. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Correct-by-Construction Cryptographic Arithmetic in Coq by Adam Chlipala ABSTRACT Cryptographic systems include big-integer arithmetic routines that have been subjected to heavy optimization, usually by hand in C or assembly code. The code is often rewritten from scratch for each new set of algorithm parameters. My collaborators and I built a tool Fiat Cryptography to automate generation of these routines, without sacrificing performance compared to the best-known C code. As a bonus, we get machine-checked proofs of correctness. The basic approach works within the Coq theorem prover, using a formally verified compiler to specialize formally verified functional programs to parameters. Today our tool is used by a number of open-source projects, including both Chrome and Firefox for producing parts of their TLS implementations. --- SPEAKER - Adam Chlipala Researcher in scaling machine-checked proofs and advanced FP ideas Adam Chlipala has been on the faculty in computer science at MIT since 2011. He did his undergrad at Carnegie Mellon and his PhD at Berkeley, and his research focuses on clean-slate redesign of computer-systems infrastructure, typically taking advantage of machine-checked proofs of functional correctness. Much of his work uses the Coq proof assistant, about which he has written a popular book, "Certified Programming with Dependent Types." He most enjoys finding opportunities for drastic simplification over incumbent abstractions in computer systems, and some favorite tools toward that end are object-capability systems, transactions, proof-carrying code, and high-level languages with whole-program optimizing compilers. Some projects particularly far along the real-world-adoption curve are Fiat Cryptography, for proof-producing generation of low-level cryptographic code, today run by Chrome for most HTTPS connections; and Ur/Web, a production-quality domain-specific language for Web applications. http://adam.chlipala.net/ --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Dimensional Analysis for Multidimensional Dataflow Programming by Monem Shennat ABSTRACT In this presentation we show an algorithm for Dimensional Analysis (DA) of a multidimensional dialect of the dataflow language Lucid. A Lucid program is a set of equations defining a family of multidimensional datasets; each data set being a collection of data points indexed by coordinates in a number of dimensions. Every variable in a Lucid program denotes one such dataset, and they are defined in terms of input and transformations applied to other variables. In general, not every dimension is relevant in every data set. It is very important not to include irrelevant dimensions because otherwise you have the same data duplicated with different values of the coordinates in the irrelevant dimension. In most multidimensional systems it is the programmer’s responsibility to exclude irrelevant dimensions and to keep track of changes in dimensionality that result from transformations. In other words, DA is performed manually. In Lucid, however, we have an alternative, namely automated DA. Static program analysis allows us to calculate or estimate the dimensionality of program variables. This is the goal of our research. We use an iterative algorithm that computes a series of approximation that settle down after a few steps. The algorithm is a first step towards the most general case; it does not yet handle local dimensions and user defined transformations. --- SPEAKER - Monem Shennat PhD student @University of Victoria, searching Dimensional Analysis for Data-flow programming Monem is studying at the Department of Computer Science in University of Victoria, working on Dimensional Analysis for Data-flow Programming for my research, and interested in analyzing and visualizing datasets. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Curious properties of latency distributions by Michał J. Gajda ABSTRACT We propose modeling of capacity insensitive distributed systems with latency distributions. We can use a latency of a single packet, and application model to get the latency of the given outcome. Using algebra of latencies we show how to efficiently computate these distributions and evaluate simple distributed systems like broadcast, or n-out-of-k majority voting. It is all implemented and illustrated by Haskell code. OBJECTIVES: Latency modeling is cheap and easy way to model performance of distributed systems. AUDIENCE: Designers of distributed systems in general: whether they are web apps, cryptocoins or swarms of Kubernetes services. --- SPEAKER - Michał J. Gajda Science-based solutions Michał got PhD in structural bioinformatics pipelines, and after two postdocs in top research facilities moved on to use his expertise of data analysis platforms in commerce. After a stint in a bank, and fintech startup, he founded his own company. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- A UML equivalent for functional programming by Yusuf Motara ABSTRACT There is currently no way to model the high-level structural design of a functional system, so just communicating about that design with dysfunctional (or OO-only) programmers is difficult. One solution is to find a modelling notation that everyone can use. But the history of UML shows that this must be done very carefully, or the results can be ... sub-optimal. This talk is about modelling and functional programming and history and language and even a little mathematics, but also about the meaning of meaning and making things as clear as possible (but no clearer). OBJECTIVES: Getting people to think about why we don't have a modelling language, and why we might want one designed by ourselves AUDIENCE: People who are interested in broadening the applicability of functional programming and making it easier to use for businesses and organizations. --- SPEAKER - Yusuf Motara Trying to make functional programming as accessible as possible Dr Yusuf Motara is a senior lecturer at Rhodes University, South Africa. His interest in teaching and using functional programming led him to consider how the functional paradigm could be made more accessible to both programmers and non-programmers, which accounts for his current interest in both modelling and gamification. Other research interests include computer science education and software development. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Effective Programming in OCaml by KC Sivaramakrishnan ABSTRACT Effect handlers have been gathering momentum as a mechanism for modular programming with user-defined effects. Effect handlers allow for non-local control flow mechanisms such as generators, async/await, lightweight threads and coroutines to be composably expressed. The Multicore OCaml project retrofits effect handlers to the OCaml programming language to serve as a modular basis of concurrent programming. In this talk, I will introduce effect handlers in OCaml, walk through several examples that illustrate their utility, describe the retrofitting challenges and how we overcome them without breaking existing OCaml code. Our implementation imposes negligible overhead on code that does not use effect handles and is efficient for code that does. Effect handlers are slated to land in OCaml after the addition of parallelism support. --- SPEAKER - KC Sivaramakrishnan Professor & Hacker at IIT Madras leading the Multicore OCaml project. KC Sivaramakrishnan is an Assistant Professor in the Computer Science and Engineering department at Indian Institute of Technology, Madras. He works on the intersection of Programming Languages and (Concurrent, Parallel, Distributed) Systems, applying the rigour of functional programming to engineer robust systems. He leads the Multicore OCaml project which brings native support for the concurrency and parallelism to OCaml. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- A Bricklayer-Tech Report by Victor Winter ABSTRACT AUTHORS: Victor Winter, Hubert Hickman, Isabella Winter Bricklayer is an educational ecosystem whose focus is on the development of visuospatial, mathematical, and computational abilities foundational to computer science. This talk gives an updated report on the core (Ed)Tech elements comprising the Bricklayer educational ecosystem. OBJECTIVE: To inform interested parties of freely available EdTech suitable for CS education AUDIENCE: Introductory CS Education --- SPEAKER - Victor Winter Creator of Bricklayer and the general-purpose transformation system TL Victor Winter is a full professor in the Department of Computer Science at the University of Nebraska-Omaha and the creator of Bricklayer. His area of expertise is programming languages. Within this area Dr. Winter has a particular interest in formalisms and frameworks that enable the description of computation in a manner that facilitates understanding as well as various forms of analysis. This interest includes, (1) verification – the informal and formal reasoning about properties of programs, and (2) validation – the manual and automated construction of tests to increase confidence in the behavior of a system. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at the virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Translating Lambda Calculus into C++ Templates by Vít Šefl ABSTRACT Template metaprogramming is an accidental feature of C++ that found its use in generic programming. However, writing metaprograms is error-prone and requires a great deal of boilerplate code. The talk explores how lambda calculus (and functional languages in general) can be used to address these problems. OBJECTIVES: Present a new way of writing template metaprograms in C++ that is clear and concise and avoids confusing template compilation errors. AUDIENCE: C++ programmers interested in functional programming --- SPEAKER - Vít Šefl PhD student researching typed FP Vít Šefl is a PhD student at Charles University. The main topic of his research is lambda calculus and typed functional programming. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at the virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Reimplementing the Wheel: Teaching Compilers with a Small Self-Contained One by Dmitry Boulytchev ABSTRACT AUTHORS: Daniil Berezun, Dmitry Boulytchev We report on a compiler construction course that is based on the idea of implementing a small self-contained compiler for a small model language from scratch, not using other compiler construction frameworks. The course is built around an evolving family of languages with increasing expressiveness and complexity, which finally is crowned by a simple language with first-class functions, S-expressions, pattern matching, and garbage collection. The code generation technique is based on the idea of symbolic interpreters, which allows to implement a robust albeit not a very efficient native code generator. OBJECTIVE: Sharing the experience in developing languages, compilers and introductory PL courses; advertising the approach; finding feedback and collaborators AUDIENCE: Tutors and researchers in the PL domain --- SPEAKER - Dmitry Boulytchev HaSCoL, OCanren, LaMa Hardware-software codesign language, miniKanren implementation for OCaml, LAmbda-ALgol, educational language Born in Krasnoyarsk in 1970. In 1980, Dmitry moved to Leningrad (now St Petersburg). In 1987, he joined the Saint Petersburg State University, where studied by turns at the Mathematics & Mechanics and Biological Faculties, until eventually graduating from the Math & Mech in 1994. In 1994-2012, he was a software developer, primarily focused on program analysis and transformations. Some notable projects include RescueWare (legacy analysis and re-engineering tool, Relativity Technologies), IntelliJ IDEA (integrated development environment, JetBrains), and HaSCoL (hardware description language, startup project). Dmitry teaches at the SPbU Software Engineering Chair since its inception in 1999, where he currently holds an associate professor position. In 2004, he defended his Ph.D. thesis "Macro-architecture Description-based Prototyping of Hardware-Software Systems" under the supervision of Prof. Andrei Terekhov. Nowadays Dmitry works as a researcher at JetBrains Research. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Teaching Automated Reasoning and Formally Verified Functional Programming in Agda and Isabelle/HOL by Jørgen Villadsen ABSTRACT We formalize two micro provers for propositional logic in Isabelle/HOL and Agda. The provers are used in an automated reasoning course at DTU where they concretize discussions of soundness and completeness. The students are familiar with functional programming beforehand but formalizing the provers, and other programs, introduces the students to formally verified functional programming in a proof assistant. Proofs that have been informal in previous courses, for instance of termination, can now be verified by the machine, and the provers provide practical examples. Similarly, the formal meta-languages provided by the formalizations clarify boundaries that can be muddled with pen and paper, for instance between syntactic and semantic arguments. We find that the automation available in Isabelle/HOL provides succinctness while the verification in Agda closer resembles functional programming. --- SPEAKER - Jørgen Villadsen Formally Verified Functional Programming Jørgen Villadsen is Associate Professor at the Department of Applied Mathematics and Computer Science of the Technical University of Denmark (DTU). His research is in logic and artificial intelligence. He is currently teaching several programming courses and an automated reasoning course. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Toward Automated Feedback in HtDP-based Programming: A DSL-based Approach by Junya Nose ABSTRACT Toward Automated Feedback in HtDP-based Programming: A DSL-based Approach AUTHORS: Junya Nose, Youyou Cong, Hidehiko Masuhara The program design recipe is a step-by-step procedure for developing programs. The design recipe breaks down a problem into smaller, more approachable tasks, but for a novice programmer, it is not always clear what to do at each design step, and whether their intermediate outcome is appropriate or not. The long-term goal of our study is to build a programming environment specialized for program development based on the design recipe. As a component of our environment, we are implementing a domain-specific language for generating feedback at intermediate steps of the design recipe. In this paper, we review existing support for design-recipe-based programming, describe the behavior of our DSL, and discuss our plans for future work. OBJECTIVE: Stimulate a discussion on novice-friendly programming environments. AUDIENCE: Educators --- SPEAKER - Junya Nose programming education, programming environment Junya Nose is a Master's student at Tokyo Institute of Technology, co-advised by Hidehiko Masuhara and Youyou Cong. He works on programming education, with special focus on functional programming. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- A generic back end for exploratory programming by Damian Frolich ABSTRACT AUTHORS: Damian Frolich and Thomas van Binsbergen Exploratory programming is a form of incremental program development in which the programmer can easily try and compare definitions, receive immediate feedback and simultaneously experiment with the language, the program and input data. Read-Eval-Print-Loop interpreters (REPLs) and computational notebooks are popular tools for exploratory programming. However, their usability, capabilities and user-friendliness are strongly dependent on the underlying interpreter and, in particular, on the ad hoc engineering required to ready the underlying interpreter for incremental program development. To break this dependency, a principled approach to REPL development can be adopted, using a so-called exploring interpreter for exploratory programming and applying software language engineering to carefully define the operational semantics of the underlying interpreter. This talk presents a generic Haskell implementation of the exploring interpreter - applicable to a large class of software languages - and demonstrates its usage to develop a variety of interfaces with a shared back-end, including command-line REPLs and a computational notebooks. OBJECTIVE: Creating excitement for exploring interpreters by showing a generic implementation of the exploring interpreter and how it can be used to develop a variety of interfaces with a shared back-end. AUDIENCE: Programming language creators, programmers and anyone in between --- SPEAKER - Damian Frolich Exploring the unknown Damian Frolich is a second year master's student doing a joint degree at the UvA and VU in Amsterdam. He is passionate about programming languages, functional programming and programmer productivity. In his free time, he likes to walk, cycle and read fantasy books. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- JIT for Dynamic Programming Languages Considered Easy by Taine Zhao ABSTRACT We start from scratch, optimising an exemplar Python program and simultaneously introducing our JIT compilation method. OBJECTIVE: Showing the audience that 1. there is an easy approach to JITing dynamic programs 2. the general-purpose JIT compiler by our approach is now available AUDIENCE: Programmers who are interested in faster dynamic programming languages, especially Python programmers. Researchers who are interested in optimisations for dynamic programming languages. --- SPEAKER - Taine Zhao General-purpose Python JIT? Is the free lunch coming? Taine Zhao is a master student at University of Tsukuba studying Programming Languages and active in open-source projects. Taine is familiar with functional programming languages such as Haskell, OCaml and F#, but also has a passion for dynamic programming languages such as Julia and Python. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Asynchronous Shared Data Sources by Mart Lubbers ABSTRACT AUTHORS: Mart Lubbers, Haye Böhm, Pieter Koopman and Rinus Plasmeijer Modern complex systems deal with a myriad of different types of data. These data sources may represent data from the system itself, a database, shared memory, external data streams or even physical data retrieved by a person. Consequently, each data source has different intrinsic properties, methods and swiftness of accessing and may therefore require each their own separate interface. Often the data needs to be massaged by a lens, combined for fusion or sequenced so that from the result of some data source, another is queried. Shared Data Sources (SDSs) are an extension of Uniform Data Sources (UDSs) and provide an atomic, uniform and composable interface over abstract data for functional languages. This abstract data can be anything ranging from data in a state, interaction with the file system to system resources such as time and random numbers. SDSs are wholly defined by their atomic read and write functions, i.e. given a linear state, they either read or write the source and yield the state again and no synchronization is required. Combinators on SDSs, as stated Parametric views extend to the original SDS idea by slightly defunctionalizing the SDS functions First-order parametric views allow a focus on shared data and an automatic lean and mean notification mechanism. With this extension, SDSs are suitable for real-life applications, that deal with a lot of data, such as coast monitoring and it is used extensively in Task Oriented Programming (TOP) frameworks such as the iTask and mTask systems to share data between tasks. This approach works very well in general but suffers from some issues. This paper proposes an extension to parametrized SDSs mitigating all these problems. --- SPEAKER - Mart Lubbers Interpreting Functional programs on microcontrollers since 2016 Mart Lubbers is a PhD student involved in Functional programming and in particular Task Oriented Programming (TOP), (embedded) domain specific language techniques and appliances of that in the Internet of Things (IoT) domain. Together with colleagues he works on mTask, a TOP language for the IoT that is fully integrated in the iTask system. Together they span all layers of the IoT. Specialized but full-fledged IoT tasks are run-time compiled to bytecode. This code is interpreted on microcontrollers and interact with the server through Shared Data Sources (SDSs) and task values as if it was a regular iTask task. This results in a major reduction of semantic friction and a lot less developer effort for the same result. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Teaching Programming to Novices Using the codeBoot Online Environment by Olivier Melançon ABSTRACT Teaching programming to novices is best done with tools with simpler user interfaces than professional IDEs that are tailored for experienced programmers. In a distance learning situation it is also important to have a development environment that is easy to explain and use, and that integrates well with the variety of course material used (slides, homework, etc). In this talk, we present codeBoot, an online programming environment which allows for fine-grained single-stepping of Python code directly in the browser. AUTHORS: Marc Feeley, Olivier Melançon Teaching programming to novices is best done with tools with simpler user interfaces than professional IDEs that are tailored for experienced programmers. In a distance learning situation it is also important to have a development environment that is easy to explain and use, and that integrates well with the variety of course material used (slides, homework, etc). In this talk, we present codeBoot, an online programming environment which allows for fine-grained single-stepping of Python code directly in the browser. OBJECTIVE: We present codeBoot and how we implemented fine-grained code single-stepping in the browser AUDIENCE: Teachers, Pythonists --- SPEAKER - Olivier Melançon M.Sc. student @ UdeM Olivier is a full stack developer, computer science college teacher and final year M.Sc student at the dynamic language research lab of Université de Montréal with Prof. Marc Feeley. He is specializing in compiler design for dynamic languages and the development of tools for teaching coding. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- Program Equivalence in Sequential Core Erlang by Péter Bereczky, Dániel Horpácsi ABSTRACT AUTHORS: Péter Bereczky and Dániel Horpácsi Our research aims to reason about the correctness of scheme-based refactoring transformations of Erlang programs. Recently, we have developed formal semantics for sequential Core Erlang in Coq in order to use it as a stepping stone towards our goal and investigate program transformations in Core Erlang. Refactoring, by definition, means transforming programs to semantically equivalent programs; thus, the correctness of the transformations depends on both the definition of semantics and how we characterize equivalence. In this extended abstract, we overview some possible formalisations of expression equivalence for Core Erlang, focusing on different kinds of simple behavioural equivalences which we have already formalised in Coq. We also show some use cases, and outline our short term future plans which include investigating other possible approaches to define program equivalence (for example contextual equivalence, and reasoning about behavioural equivalence using a dedicated logic). --- SPEAKER - Péter Bereczky Machine-checked formal semantics for verifying refactorings! Peter is an enthusiastic PhD student at Eötvös Loránd University, Budapest. His interests include formal software verification which is why he joined the High-Assurance Refactoring Project, where the goal is to reason about the meaning-preservation of refactorings considering Erlang programs. He is currently working on formalising Core Erlang and program equivalence in Coq as a stepping stone towards formalising Erlang. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - https://www.lambdadays.org/lambdadays2021 More great virtual tech conferences - https://codesync.global​ --- From FP to OO in the Classroom by Marco T. Morazán ABSTRACT How to transition from functional programming to OO programming using program by design. --- SPEAKER - Marco T. Morazán FSM CIO and a Design Recipe for all Dr. Marco T. Morazán joined Seton Hall in 1999. He did his undergraduate studies at Rutgers University and his graduate work at the City University of New York. At Seton Hall he teaches at all levels of the Computer Science curriculum including his signature courses: Introduction to Program Design I and II, Organization of Programming Languages, and Automata Theory and Computability. His main research foci are the implementation of programming languages and Computer Science Education. As the graduate school advisor, he takes special pride in making sure that his students are prepared to continue studies outside of Seton Hall. Dr. Morazán is a strong proponent of undergraduate research opportunities and routinely has students collaborate with him on projects. Along with his undergraduate research students, he is responsible for an optimal lambda lifting algorithm and an effective mechanism for closure memoization. In Computer Science education, he is especially proud of the effectiveness of the Computer Science curriculum, based on the development of video games, he has developed for beginners. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​