Welcome!

The PLEIAD laboratory of the Computer Science Department (DCC) of the University of Chile (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.

• Bounded Sort Polymorphism with Elimination Constraints accepted at POPL 2026
• Incremental Certified Programming accepted at OOPSLA 2025
• É. Tanter is on the PC of POPL 2026
• Robust Dynamic Embedding for Gradual Typing accepted at ICFP 2025
• É. Tanter has been awarded an Inria International Chair hosted by the Gallinette research team (2025-2029)
• Gradual Sensitivity Typing accepted at CSF 2025
• All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants accepted at POPL 2025
• Gradual C0: Symbolic Execution for Gradual Verification accepted at TOPLAS, to be presented at POPL 2025
• Elucidating Type Conversions in SQL Engines accepted at ESOP 2025
• Gradual Indexed Inductive Types accepted at ICFP 2024
• Gradual Differentially Private Programming published in Communications of the ACM
• Securing Verified IO Programs Against Unverified Code in F* accepted at POPL 2024

• More...

• Nico Lehmann, Assistant Professor
• Federico Olmedo, Assistant Professor
• Éric Tanter, Full Professor
• Matías Toro, Assistant Professor
• Mara Malewski, PhD student
• Damián Arquez, PhD student
• Tomás Díaz, PhD student
• Gaspar Ricci, MSc student
• José Luis Romero, MSc student