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.
schedule Submitted 1 month ago
People who liked this proposal, also liked:
Philip Wadler - (Programming Languages) in Agda = Programming (Languages in Agda)Philip WadlerProfessor of Theoretical Computer ScienceUniversity of Edinburgh
schedule 1 month agoSold Out!
BeginnerThe most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositionscorrespond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, theproof 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 weneed do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking aprogram. 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.
Harmeet Singh - Type System: The Beauty And The BeastHarmeet SinghModule Lead Software ConsultantKnoldus
schedule 2 months agoSold Out!
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
Harmeet Singh - Simplified Scala Monads And TransformationHarmeet SinghModule Lead Software ConsultantKnoldus
schedule 2 months agoSold Out!
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.