Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
people:etanter [2021/04/10 20:40]
etanter
people:etanter [2021/11/23 11:12] (current)
etanter
Line 13: Line 13:
  
 ===== News ====== ===== News ======
 +  * {{bib>​lennonAl-toplas2022|Gradualizing the Calculus of Inductive Constructions}} to appear in [[https://​dl.acm.org/​journal/​toplas|TOPLAS]],​ to be presented at [[https://​popl22.sigplan.org|POPL 2022]]
 +  * {{bib>​abateAl-toplas2021|An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation}} published in [[https://​dl.acm.org/​journal/​toplas|TOPLAS]]
 +  * {{bib>​malewskiAl-oopsla2021|Gradually Structured Data}} presented at [[https://​2021.splashcon.org/​track/​splash-2021-oopsla|OOPSLA 2021]]
   * Ten Years Most Influential Paper Award at [[https://​2020.programming-conference.org/​|<​Programming>​ 2020]] for my {{bib>​tanter:​aosd2010|AOSD 2010 paper}}   * Ten Years Most Influential Paper Award at [[https://​2020.programming-conference.org/​|<​Programming>​ 2020]] for my {{bib>​tanter:​aosd2010|AOSD 2010 paper}}
-  ​* {{bib>​abateAl-toplas2021|An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation}} to appear in [[https://​dl.acm.org/​journal/​toplas|TOPLAS]] +  * {{bib>​estepAl-ecoop2021|Gradual Program Analysis for Null Pointers}} ​presented ​at [[https://​2021.ecoop.org/​|ECOOP 2021]]
-  ​* {{bib>​estepAl-ecoop2021|Gradual Program Analysis for Null Pointers}} ​accepted ​at [[https://​2021.ecoop.org/​|ECOOP 2021]] +
-  * {{bib>​bertrandAl-arxiv2020|Gradualizing the Calculus of Inductive Constructions}}:​ check out [[https://​arxiv.org/​abs/​2011.10618|the draft]] (under revision)+
   * {{bib>​toroAl-arxiv2020|Contextual Linear Types for Differential Privacy}}: check out [[https://​arxiv.org/​abs/​2010.11342|the draft]] (under revision)   * {{bib>​toroAl-arxiv2020|Contextual Linear Types for Differential Privacy}}: check out [[https://​arxiv.org/​abs/​2010.11342|the draft]] (under revision)
-  * {{bib>​tabareauAl-jacm2020|The Marriage of Univalence and Parametricity}} ​accepted ​in the [[https://​dl.acm.org/​journal/​jacm|Journal of the ACM]] +  * {{bib>​tabareauAl-jacm2020|The Marriage of Univalence and Parametricity}} ​published ​in the [[https://​dl.acm.org/​journal/​jacm|Journal of the ACM]]
-  * {{bib>​wiseAl-oopsla2020|Gradual Verification of Recursive Heap Data Structures}} accepted at [[https://​2020.splashcon.org/​track/​splash-2020-oopsla|OOPSLA 2020]] +
-  * {{bib>​toroTanter-scp2020|Abstracting Gradual References}} accepted at Science of Computer Programming,​ to be presented at [[https://​2020.ecoop.org/​|ECOOP 2020]] +
-  * {{bib>​abateAl:​esop2020|Trace-Relating Compiler Correctness and Secure Compilation}} accepted at [[https://​www.etaps.org/​2020/​esop|ESOP 2020]] +
-  * {{bib>​diazAl:​cpp2020|A Mechanized Formalization of GraphQL}} presented at [[https://​popl20.sigplan.org/​home/​CPP-2020|CPP 2020]]+
  
- 
-===== Research Interests ===== 
- 
-    * programming and programming languages: design, semantics, implementation,​ analysis, type systems, verification 
-    * software modularity and adaptability 
-    * objects, functions, aspects, reflection, meta-programming,​ concurrency,​ distribution,​ mobility, etc. etc. 
-    * practice of programming:​ tool support, debugging, code mining, user experiments 
  
 ===== Academic Activities ===== ===== Academic Activities =====
Line 141: Line 131:
 ++++ Research Projects | ++++ Research Projects |
     * FONDECYT Project 1190058 - Gradual Reasoning About Programs: Typing, Analysis, and Verification [2019-2022/​lead]     * FONDECYT Project 1190058 - Gradual Reasoning About Programs: Typing, Analysis, and Verification [2019-2022/​lead]
-    * INRIA Équipe Associée GECO [2018-2020/lead]+    * INRIA Équipe Associée GECO [2018-2022/lead]
     * CONICYT REDES Project 170067 - CSEC: Certified Software Engineering in Coq [2018-2019/​lead]     * CONICYT REDES Project 170067 - CSEC: Certified Software Engineering in Coq [2018-2019/​lead]
     * FONDECYT Project 1150017 - Gradual Software Verification:​ Foundations and Applications [2015-2018/​lead]     * FONDECYT Project 1150017 - Gradual Software Verification:​ Foundations and Applications [2015-2018/​lead]
Line 190: Line 180:
 ++++ Grad students | ++++ Grad students |
     * [PhD] Elizabeth Labrada (gradual parametricity)     * [PhD] Elizabeth Labrada (gradual parametricity)
-    * [MSc] Damian Arquez ​(gradual sensitivity)+    * [PhD] Damian Arquez 
 +    * [PhD] Tomás Díaz  
 +    * [MSc] Tomás Vallejos [co-advised with Aidan Hogan]
     * //Former PhD students://     * //Former PhD students://
         * Raimil Cruz: [[http://​repositorio.uchile.cl/​handle/​2250/​173839|Type Abstraction and Faceted Types for Declassification]]. Defended 15/01/2020.         * Raimil Cruz: [[http://​repositorio.uchile.cl/​handle/​2250/​173839|Type Abstraction and Faceted Types for Declassification]]. Defended 15/01/2020.
Line 202: Line 194:
         * Guillaume Pothier: [[http://​repositorio.uchile.cl/​handle/​2250/​102687|Towards Practical Omniscient Debugging]]. Defended 13/06/2011.         * Guillaume Pothier: [[http://​repositorio.uchile.cl/​handle/​2250/​102687|Towards Practical Omniscient Debugging]]. Defended 13/06/2011.
     * //Former MSc students://     * //Former MSc students://
-        * Hans Fehrmann: //A Reasonably Exceptional Type Theory// [co-advised with Nicolas Tabareau]. Defended 29/12/2020.+        ​* Damián Árquez: Gradual Sensitivity Typing [co-advised with Matías Toro]. Defended 23/​11/​2021. 
 +        ​* Hans Fehrmann: [[http://repositorio.uchile.cl/​handle/​2250/​179353|A Reasonably Exceptional Type Theory]] [co-advised with Nicolas Tabareau]. Defended 29/12/2020.
         * Fabian Mosso: [[http://​repositorio.uchile.cl/​handle/​2250/​176770|Countable Polymorphic May-Must Effects]] [co-advised with Matías Toro]. Defended 12/06/2020.         * Fabian Mosso: [[http://​repositorio.uchile.cl/​handle/​2250/​176770|Countable Polymorphic May-Must Effects]] [co-advised with Matías Toro]. Defended 12/06/2020.
         * Nicolás Lehmann: [[http://​repositorio.uchile.cl/​handle/​2250/​144325|Gradual Refinement Types]]. Defended 9/​3/​2017. ​         * Nicolás Lehmann: [[http://​repositorio.uchile.cl/​handle/​2250/​144325|Gradual Refinement Types]]. Defended 9/​3/​2017. ​