Partner Event - Idris 2: Design and Implementation of a Self-Hosted Dependently Typed Language About this Event Idris is a functional programming language with dependent types. Idris 2 is a new implementation, based on Quantitative Type Theory (QTT) and implemented in Idris 2 itself. In this talk I will introduce the main features of Idris and QTT, and describe our experience with those features towards engineering a robust and efficient compiler for a dependently typed language. I will cover the trade-offs in the representation of the core language, how we use dependent types to increase our confidence in correctness of the implementation, and give an overview of the key components including evaluation, unification and type checking. Speaker Bio Edwin Brady is a Reader in Computer Science at the University of St Andrews, interested in making state of the art programming language techniques accessible to software developers and practitioners. This involves type theory, dependently typed functional programming, compilers and metaprogramming. He is currently working on a new implementation of Idris, a dependently typed functional programming language. Mar 22 2023 11.00 - 12.00 Partner Event - Idris 2: Design and Implementation of a Self-Hosted Dependently Typed Language Join Huawei and Edwin Brady for this tech talk, taking place on 22nd of March. Where (in person): : Coffee House, 4/F, Bayes Centre, 47 Potterrow, Edinburgh EH8 9BT, UK Where (virtually): https://meeting.zhumu.me/wc/96021072/join?track_id=&jmf_code=&meeting_result=&tk=&cap=d7cec&prefer=0 Registration
Partner Event - Idris 2: Design and Implementation of a Self-Hosted Dependently Typed Language About this Event Idris is a functional programming language with dependent types. Idris 2 is a new implementation, based on Quantitative Type Theory (QTT) and implemented in Idris 2 itself. In this talk I will introduce the main features of Idris and QTT, and describe our experience with those features towards engineering a robust and efficient compiler for a dependently typed language. I will cover the trade-offs in the representation of the core language, how we use dependent types to increase our confidence in correctness of the implementation, and give an overview of the key components including evaluation, unification and type checking. Speaker Bio Edwin Brady is a Reader in Computer Science at the University of St Andrews, interested in making state of the art programming language techniques accessible to software developers and practitioners. This involves type theory, dependently typed functional programming, compilers and metaprogramming. He is currently working on a new implementation of Idris, a dependently typed functional programming language. Mar 22 2023 11.00 - 12.00 Partner Event - Idris 2: Design and Implementation of a Self-Hosted Dependently Typed Language Join Huawei and Edwin Brady for this tech talk, taking place on 22nd of March. Where (in person): : Coffee House, 4/F, Bayes Centre, 47 Potterrow, Edinburgh EH8 9BT, UK Where (virtually): https://meeting.zhumu.me/wc/96021072/join?track_id=&jmf_code=&meeting_result=&tk=&cap=d7cec&prefer=0 Registration
Mar 22 2023 11.00 - 12.00 Partner Event - Idris 2: Design and Implementation of a Self-Hosted Dependently Typed Language Join Huawei and Edwin Brady for this tech talk, taking place on 22nd of March.
