List of videos

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: Writing good programs in functional languages: who, why, how? by Perdita Stevens ABSTRACT Functional programming languages have a reputation for being difficult, and functional programmers have - forgive me - a reputation for being fearsome. Why? Is there any truth in it? And how - if we wish to - could we change these reputations? My research and my teaching are both motivated by the desire to make it easier to develop good software, and my new book, "How to Write Good Programs: a guide for students" (CUP, 2020), with examples in Haskell, Java and Python, approaches the issue pragmatically. I will talk about barriers to success in functional programming, and how they might be torn down or gone round. --- SPEAKER - Perdita Stevens Professor at University of Edinburgh Perdita Stevens studied mathematics at King's College, Cambridge, and then at the University of Warwick, writing a PhD in algebra under Professor J. A. Green. She then switched to professional software engineering, working for three years at BT's Glasgow Software and Systems Engineering Centre. Here she became interested in modelling of object oriented design, and in the relationship between mathematics and software engineering. She returned to academia in 1994, taking a post as Research Fellow in the Laboratory for Foundations of Computer Science at Edinburgh. Her research interests have spanned model checking, legacy systems reengineering and games for software design; a common thread is that she likes identifying structure in systems and how it changes. From 2000-2006, she held an EPSRC Advanced Research Fellowship on Supporting Software Design. Currently, she works on mathematical aspects of software modelling and model-driven development, including foundations of bidirectionality and its potential role in democratising decisions about the behaviour of software. She wrote the first textbook on UML, Using UML, which has been translated into seven languages, and her book How to Write Good Programs was published by CUP in 2020. She has sat on over 50 international programme committees and has over 50 publications. She is on the Editorial Boards of journals including Theoretical Computer Science and Software and Systems Modeling, and has chaired conferences including UML (now MODELS), TACAS, FMOODS and FASE, and the Educators' Symposium at MODELS. She has been instrumental in the development of the bidirectional transformations community, helping organise the first Bidirectional Transformations Dagstuhl and cochairing the Bx 2013 workshop at ETAPS; she was the founding chair of the Bx steering committee. Her 2007 paper Bidirectional model transformations in QVT: Semantic issues and open questions was given the 10-year Most Influential Paper Award at MODELS 2017. In her teaching, she is particularly interested in helping students to be intrinsically motivated life-long learners. She is married (to Julian Bradfield) with a teenage son and enjoys music, especially singing. --- 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​ --- Humane Tech - Karolina Iwańska, Kamil Grondys ABSTRACT Hyperpersonalisation is not a trend anymore. It is a new normal*. With every new device, service or app a promise of fulfillment of our needs and ultimate adaptability is sold to us. What is hidden from our sight is the real purpose of the flawless software and shiny gadgets; they extort data, fight for our attention and play on individual and collective vulnerabilities. Personal security, psychological health, equal opportunities, social tissue, democracy - all those concepts can be destroyed by reckless use of technology or preserved and cherished by it. How to introduce values in the process of development of new technologies? How to make it truly humane and make sure it serves good purposes? Karolina Iwańska, a lawyer from Panoptykon Foundation and Kamil Grondys, a senior solutions architect from Samsung Electronics will present you an overview of the main ideas on the macro (EU regulation) and micro (programming team) scale. --- SPEAKERS Karolina Iwańska Panoptykon Foundation & Mozilla Fellow Karolina is a lawyer at Panoptykon Foundation, a Warsaw-based NGO fighting for human rights in the age of surveillance and member of the European Digital Rights Initiative. In 2019/20 she is also a Mozilla EU Tech Policy Fellow investigating the online advertising ecosystem and working on requirements for advertising which respects privacy and human rights. She believes it’s crucial to fight power and knowledge imbalances between people and tech platforms. panoptykon.org Kamil Grondys Solution architect at Samsung R&D Kamil is a solutions architect at Samsung R&D and cybersecurity PhD student at Warsaw University of Technology. He has been involved in Government projects related to data security. Previously he was engaged in open source communities, managed a team of developers, spoken at conferences in almost 20 countries, had guest lectures at the best Polish technical universities, as well as at Stanford University and Cape Town University. --- Lambda Days Website: https://www.lambdadays.org​ Twitter: https://twitter.com/LambdaDays​