~~NOTOC~~

====== Welcome! ======

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**.

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 =====
  * {{bib>rosainAl-popl2026|Bounded Sort Polymorphism with Elimination Constraints}} accepted at [[https://conf.researchr.org/home/POPL-2026|POPL 2026]]
  * {{bib>diazAl-oopsla2025|Incremental Certified Programming}} accepted at [[https://2025.splashcon.org/track/OOPSLA|OOPSLA 2025]]
  * É. Tanter is on the PC of [[https://conf.researchr.org/home/POPL-2026|POPL 2026]]
  * {{bib>jacobsAl-icfp2025|Robust Dynamic Embedding for Gradual Typing}} accepted at [[https://icfp25.sigplan.org/|ICFP 2025]]
  *  É. 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>arquezAl-csf2025|Gradual Sensitivity Typing}} accepted at [[https://csf2025.ieee-security.org/|CSF 2025]]
  * {{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>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>yeAl-esop2025|Elucidating Type Conversions in SQL Engines}} accepted at [[https://etaps.org/2025/conferences/esop/|ESOP 2025]]
  * {{bib>malewskiAl-icfp2024|Gradual Indexed Inductive Types}} accepted at [[https://icfp24.sigplan.org/|ICFP 2024]]
  * {{bib>toroAl-cacm2024|Gradual Differentially Private Programming}} published in [[https://cacm.acm.org/|Communications of the ACM]]
  * {{bib>andriciAl-popl2024|Securing Verified IO Programs Against Unverified Code in F*}} accepted at [[https://popl24.sigplan.org/|POPL 2024]]


  * [[news-history|More...]]

===== Members =====

  * [[people:nlehmann|Nico Lehmann]], Assistant Professor
  * [[people:folmedo|Federico Olmedo]], Assistant Professor
  * [[people:etanter|Éric Tanter]], Full Professor
  * [[people:mtoro|Matías Toro]], Assistant Professor
  * Mara Malewski, PhD student
  * Damián Arquez, PhD student
  * [[people:tdiaz|Tomás Díaz]], PhD student
  * Gaspar Ricci, MSc student
  * José Luis Romero, MSc student