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
Next revisionBoth sides next revision
research:csec [2018/03/21 10:05] – etanterresearch:csec [2018/03/21 10:07] – etanter
Line 13: Line 13:
 {{ :research:csec:kickoff-program.png?nolink&800 |}} {{ :research:csec:kickoff-program.png?nolink&800 |}}
  
-==== Titles/abstracts of the talks ====+==== Titles & abstracts of the talks (most slides are now available as well!) ====
  
 **Guillaume Munch-Maccagnoni**: **Guillaume Munch-Maccagnoni**:
Line 34: Line 34:
 **Nicolas Tabareau**: **Nicolas Tabareau**:
     * ++ Homotopy Types and Resizing Rules: a fresh look at the impredicate sort of CIC | In this talk, I will recall the basic notions of homotopy type theory and in particular the notion of homotopy n-types and of universe resizing rules, and show that it provides     * ++ Homotopy Types and Resizing Rules: a fresh look at the impredicate sort of CIC | In this talk, I will recall the basic notions of homotopy type theory and in particular the notion of homotopy n-types and of universe resizing rules, and show that it provides
-a fresh look at the impredicative universe Prop of CIC. As a consequence, I will sketch a possible extension of the Coq proof assistant with definitional proof irrelevance that is currently being implemented by Gaetan Gilbert.+++a fresh look at the impredicative universe Prop of CIC. As a consequence, I will sketch a possible extension of the Coq proof assistant with definitional proof irrelevance that is currently being implemented by Gaetan Gilbert. {{research:csec:tabareau-hott.pdf|slides}}++
     * ++ Univalent parametricity | Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it is not yet entirely clear how to extend them to handle univalence internally. In this talk, we propose a construction grounded on a univalent version of parametricity to bring the benefits of univalence to the programmer and prover, that can be used on top of existing type theories. We will present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal.++     * ++ Univalent parametricity | Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it is not yet entirely clear how to extend them to handle univalence internally. In this talk, we propose a construction grounded on a univalent version of parametricity to bring the benefits of univalence to the programmer and prover, that can be used on top of existing type theories. We will present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal.++
  
Line 44: Line 44:
  
 **Beta Ziliani**:  **Beta Ziliani**: 
-    * ++ 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.+++    * ++ 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}}++