Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Lecture
Dependent Types in Programming Languages
Description
This lecture covers different kinds of maps, type operators, equivalence of types, first-class type operators, System Fw syntax and semantics, type equivalence, the calculus of constructions, pure type systems, the lambda cube, dependent types in Coq, type universes in Coq, inductive definitions and recursion in Coq, Curry-Howard correspondence, and the equivalence between LEM and DNE. It also discusses the problem with type checking in programming languages and the adoption of dependent types in Scala and Haskell.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.