List of videos

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​