Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
research:csec [2018/03/21 10:07] etanterresearch:csec [2019/07/02 20:56] (current) etanter
Line 1: Line 1:
-====== CSEC: Certified Software Engineering in Coq / Kick-off Workshop ====== +====== CSEC: Certified Software Engineering in Coq ====== 
  
 The development of tools to construct software systems that respect a given specification is a major challenge of current and future research in computer science. Interactive theorem provers based on type theory, such as Coq, have shown their effectiveness to prove correctness of important pieces of software like the C compiler of the CompCert project. Certified programming with dependent types is attracting a lot of attention recently, and Coq is the de facto standard for such endeavors, with an increasing amount of users, pedagogical material, and large-scale projects. Nevertheless, significant work remains to be done to make Coq more usable from a software engineering point of view. The development of tools to construct software systems that respect a given specification is a major challenge of current and future research in computer science. Interactive theorem provers based on type theory, such as Coq, have shown their effectiveness to prove correctness of important pieces of software like the C compiler of the CompCert project. Certified programming with dependent types is attracting a lot of attention recently, and Coq is the de facto standard for such endeavors, with an increasing amount of users, pedagogical material, and large-scale projects. Nevertheless, significant work remains to be done to make Coq more usable from a software engineering point of view.
Line 7: Line 7:
  
  
-=== March 6-9, 2018 @ DCC, Auditorio Picarte (3er piso norte) ===+====== Kick-off Workshop: March 6-9, 2018 @ DCC ======
  
-==== Preliminary Program ====+==== Titles & abstracts of the talks ====
  
-{{ :research:csec:kickoff-program.png?nolink&800 |}}+<note new> 
 +Slides of the talks are now available! Expand the abstracts to see the link. 
 +</note>
  
-==== Titles & abstracts of the talks (most slides are now available as well!) ==== 
  
 **Guillaume Munch-Maccagnoni**: **Guillaume Munch-Maccagnoni**:
Line 38: Line 39:
  
 **Éric Tanter**: **Éric Tanter**:
-    * ++ Foundations of Dependent Interoperability | 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 work, 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 notions of type-theoretic partial Galois connections as a key foundation for dependent interoperability, which accounts for the partiality of the coercions between types. We explore the applicability of both type-theoretic Galois connections and anticonnections in the setting of dependent interoperability. A partial Galois connection enforces a translation of dependent types to runtime checks that are both sound and complete with respect to the invariants encoded by dependent types. Conversely, picking an anticonnection instead lets us induce weaker, sound conditions that can amount to more efficient runtime checks. Our framework is developed in Coq; it is thus constructive and verified in the strictest sense of the terms. Using our library, users can specify domain-specific partial connections between data structures. Our library then takes care of the (sometimes, heavy) lifting that leads to interoperable programs. It thus becomes possible, as we shall illustrate, to internalize and hand-tune the extraction of dependently-typed programs to interoperable OCaml programs within Coq itself.++ +    * ++ Foundations of Dependent Interoperability | 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 work, 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 notions of type-theoretic partial Galois connections as a key foundation for dependent interoperability, which accounts for the partiality of the coercions between types. We explore the applicability of both type-theoretic Galois connections and anticonnections in the setting of dependent interoperability. A partial Galois connection enforces a translation of dependent types to runtime checks that are both sound and complete with respect to the invariants encoded by dependent types. Conversely, picking an anticonnection instead lets us induce weaker, sound conditions that can amount to more efficient runtime checks. Our framework is developed in Coq; it is thus constructive and verified in the strictest sense of the terms. Using our library, users can specify domain-specific partial connections between data structures. Our library then takes care of the (sometimes, heavy) lifting that leads to interoperable programs. It thus becomes possible, as we shall illustrate, to internalize and hand-tune the extraction of dependently-typed programs to interoperable OCaml programs within Coq itself. {{research:csec:tanter-di.pdf|slides}}++ 
-    * ++ The Essence of Gradual Typing | Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. We present a formal foundation for gradual typing, drawing on principles from abstract interpretation, to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency—one of the cornerstones of the gradual typing approach—that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the subject-reduction proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not recourse to an externally-justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof-reduction. Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. We report on our experience applying AGT to various typing disciplines, highlighting the challenges of achieving type soundness (and not only type safety) when types are expected to enforce semantic properties like parametricity and noninterference.+++    * ++ The Essence of Gradual Typing | Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. We present a formal foundation for gradual typing, drawing on principles from abstract interpretation, to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency—one of the cornerstones of the gradual typing approach—that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the subject-reduction proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not recourse to an externally-justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof-reduction. Gradual languages designed with the AGT approach satisfy, by construction, the established criteria for gradually-typed languages. We report on our experience applying AGT to various typing disciplines, highlighting the challenges of achieving type soundness (and not only type safety) when types are expected to enforce semantic properties like parametricity and noninterference. {{research:csec:tanter-gradual.pdf|slides}}++
  
  
Line 46: Line 47:
     * ++ Towards typed-tactics in Coq: the what, the why, and the how |  The term "tactics" is heavily overloaded, sometimes meaning small-and-simple primitives of the base theory of the prover, sometimes meaning very sophisticated meta-programs. One way or another, most tactic languages provide very loose types for tactics, making them hard to compose and maintain. In this talk I will first provide some basic understanding of tactics and tactic languages, and then present the latest achievements in a new and yet fairly unexplored view of tactics: tactics typed in the base logic of the prover. In particular, I will talk about the language Mtac2, and its application in the widely-used Iris logic framework. {{research:csec:ziliani-mtac2.pdf|slides}}++     * ++ Towards typed-tactics in Coq: the what, the why, and the how |  The term "tactics" is heavily overloaded, sometimes meaning small-and-simple primitives of the base theory of the prover, sometimes meaning very sophisticated meta-programs. One way or another, most tactic languages provide very loose types for tactics, making them hard to compose and maintain. In this talk I will first provide some basic understanding of tactics and tactic languages, and then present the latest achievements in a new and yet fairly unexplored view of tactics: tactics typed in the base logic of the prover. In particular, I will talk about the language Mtac2, and its application in the widely-used Iris logic framework. {{research:csec:ziliani-mtac2.pdf|slides}}++
  
 +
 +==== Program ====
 +
 +{{ :research:csec:kickoff-program.png?nolink&800 |}}