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

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.
 
3 favorite thumb_down thumb_up 0 comments visibility_off  Remove from Watchlist visibility  Add to Watchlist
 
schedule Submitted 1 month ago

Public Feedback

comment Suggest improvements to the Speaker

  • Liked Bartosz Milewski
    keyboard_arrow_down

    Bartosz Milewski - A taste of type theory

    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 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
    Senior Developer
    MYOB
    schedule 3 days 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
    Senior Developer
    MYOB
    schedule 1 week 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.