A taste of type theory

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.

 
2 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 Philip Wadler
    keyboard_arrow_down

    Philip Wadler - (Programming Languages) in Agda = Programming (Languages in Agda)

    60 Mins
    Keynote
    Beginner
    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.
  • 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.