| Both sides previous revisionPrevious revisionNext revision | Previous revision |
| start [2021/04/06 19:10] – etanter | start [2026/01/28 22:28] (current) – etanter |
|---|
| ====== Welcome! ====== | ====== Welcome! ====== |
| |
| The [[pleiad-history|PLEIAD]] laboratory of the Computer Science Department ([[http://www.dcc.uchile.cl|DCC]]) of the [[http://www.uchile.cl|University of Chile]] ([[http://www.fcfm.uchile.cl|Faculty of Engineering]]) is a laboratory dedicated to research on software development techniques. Since its creation in 2007, the lab has focused on many ways to better support software development at different levels, from programming languages to development environments, including tools to support program understanding (debuggers, profilers, visualizers), as well as studies of the practice of programming, through mining software repositories as well as user studies.\\ | The [[https://pleiad.cl/pleiad-history|PLEIAD]] laboratory of the Computer Science Department |
| | ([[http://www.dcc.uchile.cl/|DCC]]) of the [[http://www.uchile.cl/|University of Chile]] ([[http://www.fcfm.uchile.cl/|Faculty of Engineering]]) is a laboratory dedicated to **foundational and applied research on software development techniques**. |
| |
| Currently, our work is mostly centered on **programming languages** and **program verification**. | Since its creation in 2007, the lab has focused on many ways to support the development of high-quality software at different levels, from programming languages to development environments. Currently, our work is mostly centered on **programming languages**, **program verification**, and **type theory**, as core approaches to address concerns of **correctness, efficiency, robustness, data privacy** and **security**. |
| |
| ===== Recent News ===== | ===== Recent News ===== |
| * {{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>rosainAl-popl2026|Bounded Sort Polymorphism with Elimination Constraints}} accepted at [[https://conf.researchr.org/home/POPL-2026|POPL 2026]] |
| * {{bib>estepAl-ecoop2021|Gradual Program Analysis for Null Pointers}} accepted at [[https://2021.ecoop.org/|ECOOP 2021]] | * {{bib>diazAl-oopsla2025|Incremental Certified Programming}} accepted at [[https://2025.splashcon.org/track/OOPSLA|OOPSLA 2025]] |
| * {{bib>tabareauAl-jacm2020|The Marriage of Univalence and Parametricity}} published in the [[https://dl.acm.org/journal/jacm|Journal of the ACM]] | * É. Tanter is on the PC of [[https://conf.researchr.org/home/POPL-2026|POPL 2026]] |
| * {{bib>wiseAl-oopsla2020|Gradual Verification of Recursive Heap Data Structures}} accepted at [[https://2020.splashcon.org/track/splash-2020-oopsla|OOPSLA 2020]] | * {{bib>jacobsAl-icfp2025|Robust Dynamic Embedding for Gradual Typing}} accepted at [[https://icfp25.sigplan.org/|ICFP 2025]] |
| * {{bib>toroTanter-scp2020|Abstracting Gradual References}} accepted at Science of Computer Programming, presented at [[https://2020.ecoop.org/|ECOOP 2020]] | * É. Tanter has been awarded an [[https://www.inria.fr/en/europe-and-international-schemes|Inria International Chair]] hosted by the [[https://gallinette.gitlabpages.inria.fr/website/|Gallinette]] research team (2025-2029) |
| * {{bib>abateAl:esop2020|Trace-Relating Compiler Correctness and Secure Compilation}} (Abate, Blanco, Ciobâcă, Garg, Hriţcu, Patrignani, Tanter, Thibault) accepted at [[https://www.etaps.org/2020/esop|ESOP 2020]] | * {{bib>arquezAl-csf2025|Gradual Sensitivity Typing}} accepted at [[https://csf2025.ieee-security.org/|CSF 2025]] |
| * {{bib>diazAl:cpp2020|A Mechanized Formalization of GraphQL}} (Díaz, Olmedo, Tanter) accepted at [[https://popl20.sigplan.org/home/CPP-2020|CPP 2020]] | * {{bib>poiretAl-popl2025|All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants}} accepted at [[https://conf.researchr.org/home/POPL-2025|POPL 2025]] |
| * {{bib>cruzTanter:aplas2019|Existential Types for Relaxed Noninterference}} (Cruz, Tanter) accepted at [[https://conf.researchr.org/home/aplas-2019|APLAS 2019]] | * {{bib>divincenzoAl-toplas2025|Gradual C0: Symbolic Execution for Gradual Verification}} accepted at [[https://dl.acm.org/journal/toplas|TOPLAS]], to be presented at [[https://conf.researchr.org/home/POPL-2025|POPL 2025]] |
| * {{bib>eremondiAl:icfp2019|Approximate Normalization for Gradual Dependent Types}} (Eremondi, Tanter, Garcia) accepted at [[https://icfp19.sigplan.org/|ICFP 2019]] | * {{bib>yeAl-esop2025|Elucidating Type Conversions in SQL Engines}} accepted at [[https://etaps.org/2025/conferences/esop/|ESOP 2025]] |
| * {{bib>maillardAl:icfp2019|Dijkstra Monads for All}} (Maillard, Ahman, Atkey, Martínez, Hriţcu, Rivas, Tanter) accepted at [[https://icfp19.sigplan.org/|ICFP 2019]] | * {{bib>malewskiAl-icfp2024|Gradual Indexed Inductive Types}} accepted at [[https://icfp24.sigplan.org/|ICFP 2024]] |
| * {{bib>pedrotAl:icfp2019|A Reasonably Exceptional Type Theory}} (Pédrot, Tabareau, Fehrmann, Tanter) accepted at [[https://icfp19.sigplan.org/|ICFP 2019]] | * {{bib>toroAl-cacm2024|Gradual Differentially Private Programming}} published in [[https://cacm.acm.org/|Communications of the ACM]] |
| * {{bib>cruzTanter:secdev2019|Polymorphic Relaxed Noninterference}} (Cruz, Tanter) accepted at [[https://secdev.ieee.org/2019/Home/|SecDev 2019]] | * {{bib>andriciAl-popl2024|Securing Verified IO Programs Against Unverified Code in F*}} accepted at [[https://popl24.sigplan.org/|POPL 2024]] |
| * {{bib>toroAl-popl2019|Gradual Parametricity, Revisited}} (Toro, Labrada, Tanter) accepted at [[https://popl19.sigplan.org/home|POPL 2019]] **Distinguished Paper Award** | |
| * {{bib>vazouAl-oopsla2018|Gradual Liquid Type Inference}} (Vazou, Tanter, Van Horn) accepted at [[https://conf.researchr.org/track/splash-2018/splash-2018-OOPSLA|OOPSLA 2018]] **Distinguished Paper Award** | |
| * {{bib>bodinAl-dls2018|A Trustworthy Mechanized Formalization of R}} (Bodin, Diaz, Tanter) accepted at [[https://conf.researchr.org/track/dls-2018/dls-2018/|DLS 2018]] | |
| * {{bib>toroAl-toplas2018|Type-Driven Gradual Security with References}} (Toro, Garcia, Tanter) accepted at [[https://toplas.acm.org/|TOPLAS]]/presented at [[https://popl19.sigplan.org/|POPL 2019]] | |
| * {{bib>tabareauAl-icfp2018|Equivalences for Free}} (Tabareau, Tanter, Sozeau) accepted at [[https://icfp18.sigplan.org/home|ICFP 2018]] **Distinguished Paper Award** | |
| |
| * [[news-history|More...]] | * [[news-history|More...]] |
| ===== Members ===== | ===== Members ===== |
| |
| | * [[people:nlehmann|Nico Lehmann]], Assistant Professor |
| * [[people:folmedo|Federico Olmedo]], Assistant Professor | * [[people:folmedo|Federico Olmedo]], Assistant Professor |
| * [[people:etanter|Éric Tanter]], Full Professor | * [[people:etanter|Éric Tanter]], Full Professor |
| * [[people:mtoro|Matías Toro]], Postdoc | * [[people:mtoro|Matías Toro]], Assistant Professor |
| * [[https://kenji.maillard.blue/|Kenji Maillard]], Postdoc | * Mara Malewski, PhD student |
| * [[people:elabrada|Elizabeth Labrada]], PhD student | * Damián Arquez, PhD student |
| * Stefan Malewski, PhD student | * [[people:tdiaz|Tomás Díaz]], PhD student |
| * [[people:fmosso|Fabian Mosso]], MSc student | * Gaspar Ricci, MSc student |
| * Hans Fehrmann, MSc student | * José Luis Romero, MSc student |
| * Damián Arquez, MSc student | |
| |
| |
