Lambda Ladies: International Women's Day

This video was recorded at Lambda Days 2019 http://www.lambdadays.org/lambdadays2019 Get involved in Lambda Days' next conference http://www.lambdadays.org --- KEYNOTE - USERS' PRIVACY IS IN YOUR HANDS! by Katarzyna Szymielewicz ABSTRACT Internet services promise ever faster and more intuitive online experience, often without mentioning real price and risks that come with them. Data leaks are just a small part of the problem. Data generated by algorithms or collected by applications beyond users' control have direct influence on their lives – credit score, job opportunities or exposure to biased news and advertising. GDPR [new data protection regulation] gave users stronger safeguards and new tools to protect their data. Privacy by design is no longer an aspiration - it became a requirement. But it won't become reality without people who build and design technology! Every day you make important choices that have real consequences for users' privacy. Let me convince you to use with power with a sense of responsibility. Read the full abstract: http://www.lambdadays.org/lambdadays2019/katarzyna-szymielewicz --- THE SPEAKER - KATARZYNA SZYMIELEWICZ privacy by design believer Expert in human rights and technology, lawyer and activist. Co-founder and president of Panoptykon Foundation – Polish NGO defending human rights in surveillance society. Since 2012 vice-president of European Digital Rights. From 2005 to 2009 associate at international law firm Clifford Chance, specialized in data protection and other regulatory matters. Graduate of the University of Warsaw (Law) and the School of Oriental and African Studies (Development Studies). Stipendist and member of Ashoka – international network of social entrepreneurs. More on Katarzyna Szymielewicz: http://www.lambdadays.org/lambdadays2019/katarzyna-szymielewicz --- LAMBDA DAYS & ERLANG SOLUTIONS Lambda Days is powered by Erlang Solutions. Lambda Days 2019 was sponsored by Brainly, Schibsted, Standard Chartered, Erlang Solutions, NoRedInk & Uber. LAMBDA DAYS Website: http://www.lambdadays.org Twitter: https://twitter.com/LambdaDays Facebook: https://www.facebook.com/lambdadays LinkedIn: https://www.linkedin.com/company/lambda-days/ Mail: info at lambdadays.org #LambdaDays #GDPR #privacy

This video was recorded at Lambda Days 2019 http://www.lambdadays.org/lambdadays2019 Get involved in Lambda Days' next conference http://www.lambdadays.org --- THE CODEKLAVIER CKALCUƛATOR: A LAMBDA CALCULUS CALCULATOR FOR THE PIANO by Anne Veinberg & Felipe Ignacio Noriega ABSTRACT The CKalcuƛator is a lambda-calculus arithmetic calculator for the piano and a sub-system of the CodeKlavier. The presentation will include a description of the CKalcuƛator and our motivation for bringing functional programming into the musical paradigm. Central to the presentation will be a performance by the presenters where the pianist is working with the CKalcuƛator and the results of her CKalcuƛator operations are passed onto the live coder working in SuperCollider. Read the full abstract: http://www.lambdadays.org/lambdadays2019/felipe-ignacio-noriega --- THE SPEAKER - ANNE VEINBERG CodeKlavier Anne Veinberg is an Australian pianist based in the Netherlands and is co-creator of the CodeKlavier together with Felipe Ignacio Noriega. Anne is passionate about music of and for today. She regularly collaborates with composers, actors and technologists to develop new works and musical experiences. Anne is a member of Ensemble Scala for microtonal music, of Apituley’s Locomotive Band for music theatre productions and among others. Anne also joins Felipe Ignacio Noriega to form Offzz - a live coding and piano duo. www.anneveinberg.com www.codeklavier.space More on Anne Veinberg: http://www.lambdadays.org/lambdadays2019/anne-veinberg THE SPEAKER - FELIPE IGNACIO NORIEGA CodeKlavier Felipe Ignacio Noriega is a composer, programmer and live-coding artist born in Mexico City and is co-creator of the CodeKlavier together with Anne Veinberg. He collaborates in various settings where a common subject is the incorporation of coding as a performative and aesthetic principle. The first work of the CodeKlavier, “hello world”, was the winner of the 2017 Uncaged:Conlon Foundation Composition Competition. www.felipeignacio.info www.codeklavier.space More on Felipe Ignacio Noriega: http://www.lambdadays.org/lambdadays2019/felipe-ignacio-noriega --- LAMBDA DAYS & ERLANG SOLUTIONS Lambda Days is powered by Erlang Solutions. Lambda Days 2019 was sponsored by Brainly, Schibsted, Standard Chartered, Erlang Solutions, NoRedInk & Uber. LAMBDA DAYS Website: http://www.lambdadays.org Twitter: https://twitter.com/LambdaDays Facebook: https://www.facebook.com/lambdadays LinkedIn: https://www.linkedin.com/company/lambda-days/ Mail: info at lambdadays.org #LambdaDays #calculus #music

This video was recorded at Lambda Days 2019 http://www.lambdadays.org/lambdadays2019 Get involved in Lambda Days' next conference http://www.lambdadays.org --- COMPUTER MATHEMATICS, AI AND FUNCTIONAL PROGRAMMING by Moa Johansson ABSTRACT How do you know that a mathematical proof is correct? And how do we find a nice elegant proof in the first place? Can computers help us with this? Solving mathematical problems was in fact one of the tasks adressed by the earliest AI systems developed already in the 1950’s. In this talk I will give a brief history of computer mathematics and how it connects to the development of early functional programming languages like Standard ML. I will also talk about some of my current research in how we can get computers to act creatively in the domain of mathematics; not only reason about given facts, as historically has been the case, but also invent and prove new interesting facts. To achieve this, we use tools like Haskell’s QuickCheck to allow our system, Hipster, to explore and test its way towards promising conjectures. Read the full abstract: http://www.lambdadays.org/lambdadays2019/moa-johansson --- THE SPEAKER - MOA JOHANSSON Researcher at Chalmers University Moa Johansson is an associate professor at Chalmers University in Gothenburg, Sweden. She’s interested in AI applied to mathematics and reasoning about functional programs. More on Moa Johansson: http://www.lambdadays.org/lambdadays2019/moa-johansson --- LAMBDA DAYS & ERLANG SOLUTIONS Lambda Days is powered by Erlang Solutions. Lambda Days 2019 was sponsored by Brainly, Schibsted, Standard Chartered, Erlang Solutions, NoRedInk & Uber. LAMBDA DAYS Website: http://www.lambdadays.org Twitter: https://twitter.com/LambdaDays Facebook: https://www.facebook.com/lambdadays LinkedIn: https://www.linkedin.com/company/lambda-days/ Mail: info at lambdadays.org #LambdaDays #Haskell #AI #QuickCheck

This video was recorded at Lambda Days 2020 http://www.lambdadays.org/lambdadays2020 Get involved in Lambda Days' next conference http://www.lambdadays.org Learn more about the talk: https://www.lambdadays.org/lambdadays2020/gabriele-keller Lambda Days Website: www.lambdadays.org Twitter: www.twitter.com/LambdaDays Facebook: https://www.facebook.com/lambdadays LinkedIn: https://www.linkedin.com/company/11840018/

This video was recorded at Lambda Days 2020 http://www.lambdadays.org/lambdadays2020 Get involved in Lambda Days' next conference http://www.lambdadays.org Learn more about the talk: https://www.lambdadays.org/lambdadays2020/van-anh-dam Lambda Days Website: www.lambdadays.org Twitter: www.twitter.com/LambdaDays Facebook: https://www.facebook.com/lambdadays LinkedIn: https://www.linkedin.com/company/11840018/

This video was recorded at Lambda Days 2020 http://www.lambdadays.org/lambdadays2020 Get involved in Lambda Days' next conference http://www.lambdadays.org Learn more about the talk: https://www.lambdadays.org/lambdadays2020/birthe-van-den-berg Lambda Days Website: www.lambdadays.org Twitter: www.twitter.com/LambdaDays Facebook: https://www.facebook.com/lambdadays LinkedIn: https://www.linkedin.com/company/11840018/

The bottom of the iceberg: Enabling data science research with F# This video was recorded at Lambda Days 2020 http://www.lambdadays.org/lambdadays2020 Get involved in Lambda Days' next conference http://www.lambdadays.org Learn more about the talk: https://www.lambdadays.org/lambdadays2020/evelina-gabasova Lambda Days Website: www.lambdadays.org Twitter: www.twitter.com/LambdaDays Facebook: https://www.facebook.com/lambdadays LinkedIn: https://www.linkedin.com/company/11840018/

Is Online Advertising Broken by Design? Navigating Privacy Challenges in Adtech This video was recorded at Lambda Days 2020 http://www.lambdadays.org/lambdadays2020 Get involved in Lambda Days' next conference http://www.lambdadays.org Learn more about the talk: https://www.lambdadays.org/lambdadays2020/karolina-iwanska Lambda Days Website: www.lambdadays.org Twitter: www.twitter.com/LambdaDays Facebook: https://www.facebook.com/lambdadays LinkedIn: https://www.linkedin.com/company/11840018/

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​ --- 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​

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​ --- Adventures in the browser and Node.js without writing (much) JavaScript (using PureScript) by Susan Potter ABSTRACT PureScript is an expressively typed purely functional programming language heavily inspired by Haskell yet with some key differences. Some of these differences make it more practical for web developers to exploit the Node.js and web browser ecosystems without sacrificing algebraic data types and common functional abstractions found in Haskell. We will explore through examples some of these language and ecosystem (library) differences with Haskell to see how they impact web development ergonomics and onboarding as well as describing PureScript's similarities to Haskell to contrast with TypeScript using functional libraries like fp-ts based on our experiences with all three. --- SPEAKER - Susan Potter Susan is a functional programmer working as a software engineer, architect, and hands-on manager. Over the last two decades, she has also worked on algorithmic trading systems, market data software, multi-tenant service-oriented architecture, and continuous delivery pipelines that make teams more productive. --- 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/lambdadays... More great virtual tech conferences - https://codesync.global --- Introducing Nx by Nadia Polikarpova ABSTRACT Program synthesis is a promising approach to automating low-level aspects of programming by generating code from high-level declarative specifications. But what form should these specifications take? In this talk I will advocate for using types as input to program synthesis. Types are widely adopted by programmers, they can vary in expressiveness and capture both functional and non-functional properties, and finally, type checking is often fully automatic and compositional, which helps the synthesizer find the right program. I will describe two type-driven program synthesizers we developed. The first one is Synquid, a synthesizer for recursive functional programs that uses expressive refinement types as a specification mechanism. The second one is Hoogle+, which relies on more mainstream Haskell types and generates code snippets by composing functions from Haskell libraries. --- SPEAKER - José Valim Nadia Polikarpova is an assistant professor at UC San Diego, and a member of the Programming Systems group. She received her Ph.D. in Computer Science from ETH Zurich in 2014, and then spent a couple years as a postdoctoral researcher at MIT. Nadia's research interests are in program synthesis, program verification, and type systems. She is a 2020 Sloan Fellow, and a recipient of the 2020 NSF Career Award and the 2020 Intel Rising Stars Award. --- 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 Functional Programming: the Glue for Introducing Computing through Data Science by Kathi Fisler | ABSTRACT The "language wars" about the best way to teach programming are alive and well. They're also moving into new territory. Many countries are ramping up computing education for K-12. Disciplines across universities are looking to develop Data Science abilities in their students. Leaders emphasize having these efforts reach students equitability, lest we increase digital divides. Which languages, curricula, pedagogies, and tools would help us meet those goals? Luckily for the fun()ky folks like those as Lambda Days, we have a lot of experience, as well as educational research, showing the value of functional programming in these broader settings. By summarizing what we already know from these efforts, I hope to leave everyone with fresh talking points about the centrality of functional programming to holding these values together in computing education. • 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 talk was recorded at Lambda Days 2023. If you're curious about our upcoming event, check https://lambdadays.org ✨ Although delimited continuations are not a new idea, they have recently seen renewed interest from several programming language communities as a powerful tool for implementing schedulers and effect systems. Unfortunately, there is a major remaining obstacle to their adoption, namely that most programmers find them utterly opaque. To help fix that, this talk provides an overview of what delimited continuations are, how they work, and why they’re useful from a perspective accessible to the working programmer. Let's keep in touch! Follow us on: Twitter: https://twitter.com/LambdaDays LinkedIn: https://www.linkedin.com/company/lambda-days Facebook: https://www.facebook.com/lambdadays

✨This talk was recorded at Lambda Days 2023. If you're curious about our upcoming event, check https://lambdadays.org ✨ 🎶Creating software is like composing a symphony, Every note a line of code and every abstraction a harmony. Layering instruments and sounds, we carefully craft our piece, Adding in features that bring our work to life and (hopefully) prod release. But the right command we must click to create a unified sound, or else we try to put it all together but no rhythm will be found🎶 As software composers, when we create documentation arrangements to guide others in performing our piece our job becomes significantly easier and our prose becomes much more effective if we begin by considering our users' interests, needs and experience levels. This results in higher-quality documentation, blog posts and technical presentations. OBJECTIVES After this session, you will know how to compose documentation and other software artefacts that empower your audience and improve the adoption and support of your product. Slides: https://www.lambdadays.org/lambdadays2023/ Let's keep in touch! Follow us on: 💥Twitter: https://twitter.com/LambdaDays 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync

✨This talk was recorded at Lambda Days 2023. If you're curious about our upcoming event, check https://lambdadays.org ✨ Are you tired of staring at a screen full of confusing error messages when working with a LISP? This talk will focus on the common patterns of errors in the language and teach attendees how to quickly recognize and troubleshoot them. We will specifically be using Clojure as our example language, but the concepts and techniques covered can be applied to other LISP languages. Through real-world examples, and my personal experiences, attendees will gain valuable insights and practical tips for improving their code and becoming more efficient at debugging. Whether you're a seasoned Clojure developer or just getting started, you won't want to miss this fun and informative session on mastering the art of error handling in LISP. Let's keep in touch! Follow us on: 💥Twitter: https://twitter.com/LambdaDays 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync

Discover Functional Females: a community for Females in Functional Programming to collaborate, pursue connection and seek support. Let's keep in touch! Follow us on: 💥Twitter: https://twitter.com/LambdaDays 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://mastodon.social/@codesync

✨ This keynote talk was recorded at Lambda Days 2024. Join our Waiting List for 2025 and be part of the event next time! https://lambdadays.org ✨ Abstract I published my first paper on modelling telecoms protocols in 1989 and then implemented an interpreter for protocol languages in David Turner’s Miranda. As a consequence, I fell in love with functional programming, and I learned about the power of making equations come to life. But for me these are means to an end; it is the role of models and reasoning about them that are my focus. The types of models and techniques I have developed and used have changed over the years, and so have I. These days, my models are usually probabilistic and often developed in Milner’s Bigraphs (with extensions). Using several examples, from systems biology to mixed reality systems, I will reflect on how my research has evolved, what I have learned, and some challenges and issues we might think about in the future. Let's keep in touch! Follow us on: 💥Twitter: https://twitter.com/LambdaDays 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync

✨ This keynote talk was recorded at Lambda Days 2024. Join our Waiting List for 2025 and be part of the event next time! https://lambdadays.org ✨ Abstract Algebraic effects and handlers are a powerful way to incorporate effects in programming languages. Algebraic effect handlers can express any free monad in a concise and composable way, and can be used to express complex control-flow, like exceptions, asynchronous I/O, local state, backtracking, and many more. However, existing designs of algebraic effects often require effects to be executed sequentially. In this talk, I give an overview of algebraic effect handlers, and discuss how to combine effect handlers with parallelizable computations. Let's keep in touch! Follow us on: 💥Twitter: https://twitter.com/LambdaDays 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync

✨ This talk was recorded at Lambda Days in June 2024. If you're curious about our upcoming event, check https://lambdadays.org ✨ At some point, a business may reach a stage where app logic should be executed based on specific conditions like location, app version, or user type. For example, you may have to dynamically change discounts to sell leftover stock or limit low-profit requests during peak hours. Each new “crazy” idea from your manager often means coding, understanding needs, and system load with frequent redeployments. From a business perspective, as a manager, you want the ability to control the system's behavior without struggling through endless discussions, tickets, and running a full development cycle. We will design a rule matcher to manage changing conditions in real-time in a user-friendly manner. It will use any app traffic attribute, verify rule validity, and keep rules easy to read and manage. We will leverage the capabilities of Scala and recursion schemes to create a fast and efficient solution that can be integrated into any app. Let's keep in touch! Follow us on: 💥BlueSky: https://bsky.app/profile/lambdadays.bsky.social 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync 💥Twitter: https://twitter.com/LambdaDays

✨ This talk was recorded at Lambda Days in June 2024. If you're curious about our upcoming event, check https://lambdadays.org ✨ We are constantly looking for different ways to make communication across the stack in our Web apps easier: GraphQL lets frontend developers write queries directly for the data they need, React Server Components make it possible to render the static parts of a SPA on the server, and Phoenix LiveView runs entire interactive applications on the backend. Lustre is a frontend framework for Gleam, a new statically typed functional programming language that compiles to both Erlang and JavaScript. Lustre exploits the similarities between The Elm Architecture and Erlang's actor model to enable fully universal components. In this talk we'll take a look at Gleam, explore Lustre's application architecture, and demonstrate how components really can be "write once, run everywhere. Let's keep in touch! Follow us on: 💥BlueSky: https://bsky.app/profile/lambdadays.bsky.social 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync 💥Twitter: https://twitter.com/LambdaDays

✨ This talk was recorded at Lambda Days in June 2024. If you're curious about our upcoming event, check https://lambdadays.org ✨ Elm is a strongly typed, purely functional DSL described by its creator as a "delightful language for reliable web applications". A couple years back, frustrated with my limited but already painful experiences with React and Vue, I did what any sane developer would. After spending all of 20 minutes playing with in-browser tutorials, I opted to make Elm the main language for my next project. In this talk, I will reflect on my experience building and growing a 10k LOC Elm codebase. Most importantly, I hope to convince you that Elm is awesome and that frontend development needs not be the lawless, weakly typed wasteland it first appears to be. Let's keep in touch! Follow us on: 💥BlueSky: https://bsky.app/profile/lambdadays.bsky.social 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync 💥Twitter: https://twitter.com/LambdaDays

✨ This talk was recorded at Lambda Days in June 2024. If you're curious about our upcoming event, check https://lambdadays.org ✨ Abstract WasmRef-Isabelle is a WebAssembly interpreter written in Isabelle/HOL verified to be sound with respect to the WasmCert-Isabelle mechanisation of WebAssembly. Its main improvement on both the existing verified interpreter included in WasmCert-Isabelle and even the official (but unverified) WebAssembly reference interpreter is in performance – in fact, thanks to that, the Wasmtime (one of the main WebAssembly implementations) team adopted it as their fuzzing oracle. So, how much direct effort does it take to achieve such a practical result in formal verification? Actually, not an insane amount. I'll talk about how we verified WasmRef-Isabelle as a two-step refinement proof, using the WasmCert-Isabelle interpreter as the springboard so to speak, in a single (one-year) master's thesis time. Let's keep in touch! Follow us on: 💥Twitter: https://twitter.com/LambdaDays 💥LinkedIn: https://www.linkedin.com/company/lambda-days 💥Facebook: https://www.facebook.com/lambdadays 💥Mastodon: https://genserver.social/codesync