0:00 / 0:00

2022 LLVM Dev Mtg: MLIR for Functional Programming

Name: 2022 LLVM Dev Mtg: MLIR for Functional Programming
Uploaded: 2022-12-09T01:02:42Z
Duration: 24 min 11 s
Channel: LLVM
Description: Siddharth Bhat discusses implementing an MLIR-based backend for the Lean4 proof assistant and encoding functional programming concepts in SSA style.

LLVM

18K subscribers • 15 videos on Hallway

YouTube

Recommended by 1 person: 1 in engineering communities.
Presented by Siddharth Bhat
Linked in the descriptionleanprover/lean4 Slides on llvm.org arXiv 2201.07272

Advanced. Deep dive for people who know the field.

3.2K views3 years ago1 recommendation

Programming languages Systems programming Compilers and interpreters Functional programming

Siddharth Bhat discusses implementing an MLIR-based backend for the Lean4 proof assistant and encoding functional programming concepts in SSA style.

2022 LLVM Developers' Meeting llvm.org/devmtg/2022-11/ ------ MLIR for Functional Programming Speaker: Siddharth Bhat ------ Slides: llvm.org/devmtg/2022-11/slides/TechTalk15-ShortLambdatheUlti… ----- In this talk, we discuss the implementation, upstreaming, and community concerns of adoption LLVM and MLIR within the Lean4 proof assistant, and more broadly, discuss takeaways for MLIR to have strong support for functional programming languages. We walk through the process of creating a new MLIR-based backend for Lean4, a dependently typed programming language. We demonstrate our MLIR dialect (arxiv.org/abs/2201.07272) which encode core functional programming concepts within the SSA style. However, having a fully functional backend is not enough; We discuss the worries around MLIR adoption in the Lean4 community, and the discussions that led to Lean4 choosing to adopt LLVM for the time being. We discuss our current LLVM backend effort for Lean4 (github.com/leanprover/lean4/pull/1497), and end with a discussion of how the MLIR community could help with the adoption of MLIR for functional programming languages. ----- Videos Edited by Bash Films: BashFilms.com

Why it's here

1 person recommends this

What people say. Recommended as an explanation of using SSA and MLIR for functional programming languages.

Moments people linked to

u/Psychosqrin r/ProgrammingLanguages • 3 years agoRecommends

Is continuation passing style conversion still used as an intermediate language? Hello, I am curious if cps is still used as an intermediate language? I’d like to read “compiling with continuations”. What are some better IRs now if any? Cps conversion is for functional languages for the most part. On the llvm YouTube channel there was a talk about using ssa for functional languages. Here’s the video link to this video Is ssa the future for functional languages? Anyways any tips will be appreciated. Thanks

67View on Reddit