Thursday 14 September 2017, 10:30, LSV: Foundations of Dependent Interoperability, Pierre-Evariste Dagand (CNRS, LIP6).
Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading static guarantees for runtime checks, the "dependent interoperability" framework provides a mechanism by which simply-typed values can safely be coerced to dependent types and, conversely, dependently-typed programs can defensively be exported to a simply-typed application.
In this talk, we give a semantic account of dependent interoperability. Our presentation relies on and is guided by a pervading notion of type equivalence, whose importance has been emphasized in recent work on homotopy type theory. Specifically, we develop the notion of "type-theoretic Galois connections" as a key foundation for dependent interoperability, which accounts for the partiality of the coercions between types.
This is joint work with Eric Tanter and Nicolas Tabareau.