~~NOTOC~~

====== 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. 
Currently, our work is mostly centered on **programming languages**, **program verification**, and **type theory**.

===== Recent News =====
  * {{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]]
  * 10-year Most Notable Paper Award at DLS 2023 for our DLS 2013 paper {{bib>allendeAl-dls2013|Cast Insertion Strategies for Gradually-Typed Objects}} (Allende, Fabry, Tanter)
  * {{bib>yeAl-oopsla2023|A Gradual Probabilistic Lambda Calculus}} accepted at [[https://2023.splashcon.org/track/splash-2023-oopsla|OOPSLA 2023]]
  * New Inria Associate Team [[https://pleiad.github.io/grapa-website/|GRAPA]] (Gradual Proof Assistants) funded for 2023-2025
  * {{bib>toroAl-toplas2023|Contextual Linear Types for Differential Privacy}} appears in [[https://dl.acm.org/journal/toplas|TOPLAS]]

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

===== Members =====

  * [[people:folmedo|Federico Olmedo]], Assistant Professor
  * [[people:etanter|Éric Tanter]], Full Professor
  * [[people:mtoro|Matías Toro]], Assistant Professor
  * Koen Jacobs, Postdoc (with Inria)
  * Stefan 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