(Programming Languages) in Agda = Programming (Languages in Agda)

schedule May 15th 09:00 - 10:00 AM place Red Room people 185 Interested

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.

 
7 favorite thumb_down thumb_up 0 comments visibility_off  Remove from Watchlist visibility  Add to Watchlist
 

Target Audience

Programmers

schedule Submitted 5 months ago

  • Liked Bartosz Milewski
    keyboard_arrow_down

    Bartosz Milewski - A Taste of Type Theory

    Bartosz Milewski
    Bartosz Milewski
    Math Evangelist
    Programming Cafe
    schedule 5 months ago
    Sold Out!
    60 Mins
    Keynote
    Beginner

    We use types in programming, often without realizing how deeply rooted they are in the foundations of mathematics. There is a constant flow of ideas from type theory to programming (and back). We are familiar with algebraic data types; inductive types, like lists or trees; we've heard of dependent types and, in the future, we might encounter identity types and possibly get familiar with elements of homotopy type theory. I can't possibly talk about all of this, but I'll try to give you a little taste.

  • Liked Edward Kmett
    keyboard_arrow_down

    Edward Kmett - Logic Programming à la Carte

    30 Mins
    Invited Talk
    Beginner
    I've been working on a logic programming framework in Haskell, called guanxi (關係) with an eye towards scalability. To build it I leaned heavily on my previous work on propagators and a bunch of other little bits and pieces of algebra and category theory in the design process. A number of patterns have arisen repeatedly throughout the process of building this library. I'll give a tour through the current state of guanxi and try to extract some of the more reusable bits of its design for your inspection.
  • Liked Philip Wadler
    keyboard_arrow_down

    Philip Wadler - Programming Language Foundations in Agda

    90 Mins
    Code Jam
    Advanced

    PARTICIPANT PREPARATION:

    Clone the repository at

    https://github.com/plfa/plfa.github.io/

    This is the textbook for the course.

    Install Agda, the Agda standard library, and configure the plfa library. This can be done by following the instructions under the heading

    Getting Started with PLFA

    at

    https://plfa.github.io/GettingStarted/

    Outline:

    This course is an introduction to formal methods in Agda, covering datatypes, recursion, structural induction, indexed datatypes, dependent functions, and induction over evidence; with focus on formal definitions of naturals, addition, and inequality, and their properties.

    The textbook is freely available online:

    • Programming Language Foundations in Agda
      plfa.inf.ed.ac.uk
      github.com/plfa/plfa.github.io/

    The book has been used for teaching by me at:

    • University of Edinburgh (Sep-Dec 2018)
    • Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio) (Mar-Jul 2019)
    • University of Padova (Jun 2019)

    and by others at

    • University of Vermont
    • Google Seattle.

    The book is described in a paper (of the same title) at the XXI
    Brazilian Symposium on Formal Methods, 28--30 Nov 2018, which is
    available here:

    http://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf

    The paper won the SBMF 2018 Best Paper Award, 1st Place.

  • Liked Edward Kmett
    keyboard_arrow_down

    Edward Kmett / Tony Morris - Let's Lens

    480 Mins
    Introductory Workshop
    Beginner

    Let's Lens presents a series of exercises, in a similar format to the Data61 functional programming course material. The subject of the exercises is around the concept of lenses, initially proposed by Foster et al., to solve the view-update problem of relational databases.

    The theories around lenses have been advanced significantly in recent years, resulting in a library, implemented in Haskell, called lens.

    This workshop will take you through the basic definition of the lens data structure and its related structures such as traversals and prisms. Following this we implement some of the low-level lens library, then go on to discuss and solve a practical problem that uses all of these structures.

  • Liked Attila Egri-Nagy
    keyboard_arrow_down

    Attila Egri-Nagy - Approaching the Yoneda Lemma

    30 Mins
    Talk
    Intermediate

    The Yoneda lemma is not the first thing to learn in category theory, but sooner or later it appears in studying the field. Unfortunately, there is quite a gap between the intuitive idea, "tell me your friends, and I will know who you are" , and its precise formulation. This talk aims to bridge this gap by introducing algebraic results in the middle, namely Cayley's theorem for groups and its generalization to semigroups. These are elementary enough, but at the same time they exhibit the conceptual step of representability, and the idea of studying all different things in a familiar form.

  • Liked Andy Kitchen
    keyboard_arrow_down

    Andy Kitchen - Meta-quines

    30 Mins
    Talk
    Beginner

    A quine is a program that outputs its own source code, but can you create a 2 quine, a pair of programs that output each other with an A->B->A->B cycle? What about between different languages? Can you gzip your own source code? Is there a structured way to do this with theory? All these questions will be somewhat answered, in ways that will make your head hurt... math-a-magical demos and over 9000 layers of meta-ness await!

  • Liked Xuanyi Chew
    keyboard_arrow_down

    Xuanyi Chew - An Alien Lambda Calculus

    Xuanyi Chew
    Xuanyi Chew
    Chief Data Scientist
    Ordermentum
    schedule 3 months ago
    Sold Out!
    30 Mins
    Talk
    Beginner

    The conventional wisdom in functional programming communities is that lambda calculus was "discovered". Extending the logic of the statement to its extreme, we might propose that an alien would recognize lambda calculus as a computational model. But would we be able to recognize an alien lambda calculus?

    This talk is part gedankenexperiment, part speculative fiction, part practical advice on compiler design. We begin by imagining ourselves to be creatures in a universe which is very different from the one we're in, except the notion of consciousness and intelligence are preserved from our current universe. From there, we shall explore the physics and alternate philosophies that would yield an alien lambda calculus.

    Of course, being from an alien conception, there are some questions that must be answered - in the name of practicality, is there perhaps even a weak notion of a functor from the alien lambda calculus to that of the one we know today? Is there anything from the alien lambda calculus that we may yield and put into practice? And what is this pesky business with state? Isn't the point of functional programming to hide states from the programmer by abstracting over them? Or was it to make clear the states? And what of names? Isn't lambda purely anonymous?

  • Liked Ken Scambler
    keyboard_arrow_down

    Ken Scambler - Applied Category Theory - The Emerging Science of Compositionality

    Ken Scambler
    Ken Scambler
    Software Architect
    MYOB
    schedule 6 months ago
    Sold Out!
    30 Mins
    Talk
    Intermediate

    What do programming, quantum physics, chemistry, neuroscience, systems biology, natural language parsing, causality, network theory, game theory, dynamical systems and database theory have in common?

    As functional programmers, we know how useful category theory can be for our work - or perhaps how abstruse and distant it can seem. What is less well known is that applying category theory to the real world is an exciting field of study that has really taken off in just the last few years. It turns out that we share something big with other fields and industries - we want to make big things out of little things without everything going to hell! The key is compositionality, the central idea of category theory.

    This talk will introduce the emerging field of applied category theory, with the aims of:

    • Giving attendees a broad overview of cutting-edge applications of category theory
    • Building an understanding of a small number of the most important core concepts
    • Getting attendees excited, inspired to learn more, and equipped to apply some basic concepts to their work

  • Liked Attila Egri-Nagy
    keyboard_arrow_down

    Attila Egri-Nagy - The rules of the game

    30 Mins
    Talk
    Beginner

    In the post-AlphaGo era there is no need for introducing the game of Go. It is one of the most complex games with very simple rules. But wait a minute, how simple are they exactly? ... different solutions for a problem with clashing requirements, leading to endless debates; edge cases where specifications offer no help; complexity hopeless to tame... Are we still talking about the game, or about software development?!? Well, both. This may come as a surprise, but there is no agreement on the rules of Go. The different rule sets are compatible most of the time, but when they disagree, they do it in a big way in deciding who is the winner. Can we fix the rules then? There are researchers working on the problem, but the perfect rule set is as elusive as the perfect software application.

    This talk is a cautionary tale about the power and limits of formalization, and how humans relate to formal specifications. We will discuss the different rule sets, analyze their differences. The `simple' case of Go will serve as an analogue for software specifications and foundations of Mathematics.

  • Liked Harmeet Singh
    keyboard_arrow_down

    Harmeet Singh - Type System: The Beauty And The Beast

    30 Mins
    Talk
    Intermediate

    Type System plays an important role in building type-safe applications which reduce immense runtime exceptions and developer mistakes. This sophisticated system is leverage by Scala’s most famous functional libraries like Scala-Cats and ScalaZ. This feature-rich system allows implementing pure Functional programming on JVM. It is a beast due to its complex syntax as it prevents developers to explore its beautiful aspects like partial types in Scala. In this talk, we’d be taming the beast and use its beauty to solve real-life issues faced during coding

  • Liked Harmeet Singh
    keyboard_arrow_down

    Harmeet Singh - Simplified Scala Monads And Transformation

    30 Mins
    Talk
    Beginner

    Keeping the functional paradigm intact while using complicated monad structure in your code could be quite a tedious task. Especially, when your business logic needs to be structured in a flow, suddenly you realize that your code is moving away from the functional paradigm. Well, definitely Monads composition is the savior in this kind of situations, however, composing them practically is again a cumbersome task. We will be jumping into some coding examples in this talk, which would hopefully make you sit back and relax when you face this kind of situation again. We will create custom monads, right usage of monadic operator and resolution of monad composition problems and monads transformation with some real-life scenarios and examples.

  • Liked Jichao Ouyang
    keyboard_arrow_down

    Jichao Ouyang - Building blocks reactive UI with <&> <+> flatMap ... in Scala.js

    Jichao Ouyang
    Jichao Ouyang
    Sr. Developer
    MYOB
    schedule 4 months ago
    Sold Out!
    90 Mins
    Workshop
    Beginner

    This is a hands-on workshop to show how Typed Spreadsheet Programming library Owlet and Cats typeclasses can help making Reactive UI functional and simple just like how you'd get thing done in spreadsheet.

  • Liked Jichao Ouyang
    keyboard_arrow_down

    Jichao Ouyang - Functional "Design Pattern"? ReaderT, MTL or Free Monad? Why not all?

    Jichao Ouyang
    Jichao Ouyang
    Sr. Developer
    MYOB
    schedule 4 months ago
    Sold Out!
    30 Mins
    Talk
    Intermediate

    Functional Programming in practice always end up in question of how to properly abstract effects from pure, testable, rationale business.

    Some believe ReaderT is all you need to abstract your effects, some believe that MTL has enough transformers to transform your effects, some believe IO can do all these jobs and much performant, others believe it's best to be able to freely abstract what ever effects they can imagine

    But in the real world, when you create a practical industry project that need to scale, as the code base get lager, more effects we will have/need, and much clearer that different cake layers of these 3 technique will fell into

    So, eventually we need all of these approaches to server different layer of abstractions, and hence the reason I'm working on luci(鸕鶿) recently.