Programming Languages and Systems

We aim to make programming simpler, more efficient, more accessible and trustworthy.

Our tools shape how we think and what we can do. A new way of thinking about programming can make complex problems disappear, while a different programming paradigm or a novel implementation can enable new capabilities that were previously hard to imagine.

Our group works on understanding, designing and implementing programming languages and systems that make programming simpler, more efficient, more accessible and trustworthy.

We are interested in programming systems ranging from conventional programming languages to tools used by data scientists and end-user programming systems. We leverage a variety of methods, including programming langauge theory, empirical studies of programming tools, but also human-computer interaction and interdisciplinary approaches.

Curious about what we are currently working on? Check out our ongoing research projects on GitHub!

We co-organize the Prague Prog­ramming Languages and Systems Research Network. Check it out and sign up to get updates about events!

Research Projects

Tools for Data-Centric Programming

Data scientists have to rely on error-prone tools that do not support good engineering principles. Our goal is to develop rigorous methodologies and tools that increase our confidence in results while retaining ease of use.

We rely on empirical analysis of large code repositories, develop new program analysis techniques and new notions of types suitable for data-centric programs.

Proof Assistants for Semantics Engineering

Semantics engineering tools let researchers interactively explore their definitions, while proof assistants can be used to check their properties. Our goal is to integrate the two kinds of tools into a more powerful interactive system.

We aim to create tools that eliminate boilerplate from proofs, but also use insights from the exploration of executable semantics in proof construction.

Interactive Programming Systems

Programming languages are only a small part of programming. Today, programming is often done by interacting with rich stateful systems.

We aim to adapt existing programming language ideas for the context of programming systems, develop new basic methods for studying programming systems and use those in practically important domains.

History and Philosophy of Programming

Programming tools have evolved significantly over the past decades, but our conceptual understanding remains rooted in ideas over 60 years old.

We need an interdisciplinary methodology that uncovers basic methodological assumptions, explains the origins of our present thinking, finds alternative paths, and leverages them to develop new programming paradigms.

People

Aleks Boruch-Gruszecki
Postdoc
Type Systems, Knowledge Management, AI
e-mail: research@abgru.me
Joel Jakubovic
Postdoc
Graphical Constraint Programming for Notational Freedom
e-mail: jakubovic@d3s.mff.cuni.cz
Tomáš Petříček
Assistant professor
Programming Systems and Languages, History and Philosophy of Computing
e-mail: petricek@d3s.mff.cuni.cz
Vít Šefl
Ph.D. student
Functional Programming, Type Systems
e-mail: sefl@ksvi.mff.cuni.cz
Jan Liam Verter
Ph.D. student
Proof Assistants, Type Systems, Programming Systems and Languages
e-mail: verter@d3s.mff.cuni.cz
Jan Vitek
Professor
Programming Systems and Languages
e-mail: vitekj@me.com

Student Projects

Our students have successfully defended theses on a number of interesting topics including type systems, new programming language design, as well as history of programming and new programming experiences. If you are interested in joining us for a student project check out our student project and theses topic areas.

AgentLang - Programming Language for Agent-based Modeling

Tomáš Boďa

Bachelor's thesis (2023/24)

Read the thesis text

Look at the defence poster

Check out demo or source

Design of LLM prompts for iterative data exploration

Mikoláš Fromm

Bachelor's thesis (2023/24)

Read the thesis text

Look at the defence poster

Check out demo or source

Reconstructing the Pygmalion programming environment

Adrián Habušta

Bachelor's thesis (2023/24)

Read the thesis text

Look at the defence poster

Check out demo or source

Abstract interpretation of pandas

Jan Hrubý

Bachelor's thesis (2023/24)

Read the thesis text

Look at the defence poster

Check out demo or source

Query langauge for relational databases

David Koňařík

Bachelor's thesis (2023/24)

Read the thesis text

Look at the defence poster

Check out demo or source

Combining effects with dependent types

Maya Mückenschnabel

Bachelor's thesis (2023/24)

Read the thesis text

Look at the defence poster

Recent Publications

Link bibtex
J. Belyakova, B. Chung, R. Tate, J. Vitek:
Decidable Subtyping of Existential Types for Julia, in Proc. ACM Program. Lang. 8(PLDI), pp. 191:1091–191:1114, 2024
DOI: 10.1145/3656421
Link bibtex
Y. Xu, A. Boruch-Gruszecki, M. Odersky:
Degrees of Separation: A Flexible Type System for Safe Concurrency, in Proc. ACM Program. Lang. 8(OOPSLA1), pp. 136:1181–136:1207, 2024
DOI: 10.1145/3649853
Link bibtex
T. Petříček:
Language and the Rise of the Algorithm by Jeffrey M. Binder (review), in Technology and Culture 65(1), pp. 427-429, 2024
Link bibtex
P. Maj, S. Muroya, K. Siek, L. Di Grazia, J. Vitek:
The Fault in Our Stars: Designing Reproducible Large-scale Code Analysis Experiments, in DROPS-IDN/v2/document/10.4230/LIPIcs.ECOOP.2024.27, 2024
DOI: 10.4230/LIPIcs.ECOOP.2024.27
Link bibtex
L. Parreaux, A. Boruch-Gruszecki, A. Fan, C. Chau:
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism, in When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism (Artifact) 8(POPL), pp. 48:1418–48:1450, 2024
DOI: 10.1145/3632890
Link bibtex
T. Petříček, G. Burg, A. Nazábal, T. Ceritli, E. Jiménez-Ruiz, C. Williams:
AI Assistants: A Framework for Semi-Automated Data Wrangling, in IEEE Transactions on Knowledge and Data Engineering 35(9), pp. 9295-9306, 2023
DOI: 10.1109/TKDE.2022.3222538
Link bibtex
A. Boruch-Gruszecki, M. Odersky, E. Lee, O. Lhoták, J. Brachthäuser:
Capturing Types, in ACM Trans. Program. Lang. Syst. 45(4), pp. 21:1–21:52, 2023
DOI: 10.1145/3618003
Link bibtex
P. Taylor-Gooby, T. Petříček, J. Cunliffe:
Covid19, Charitable Giving and Collectivism: a data-harvesting approach, in Journal of Social Policy 52(3), pp. 473-494, 2023
DOI: 10.1017/S0047279421000714
Link bibtex
J. Edwards, T. Petříček, T. van der Storm:
Live & Local Schema Change: Challenge Problems, in , 2023
DOI: 10.48550/arXiv.2309.11406
Link bibtex
M. Mehta, S. Krynski, H. Gualandi, M. Thakur, J. Vitek:
Reusing Just-in-Time Compiled Code, in Artifact of "Reusing Just-in-Time Compiled Code" 7(OOPSLA2), pp. 263:1176–263:1197, 2023
DOI: 10.1145/3622839
Link bibtex
J. Jakubovic, J. Edwards, T. Petříček:
Technical Dimensions of Programming Systems, in The Art, Science, and Engineering of Programming 7(3), pp. 13:1-13:59, 2023
DOI: 10.22152/programming-journal.org/2023/7/13
Link bibtex
A. Boruch-Gruszecki, R. Waśko, Y. Xu, L. Parreaux:
A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoning, in Mechanized proof of «A case for DOT: Theoretical Foundations for Objects With Pattern Matching and GADT-style Reasoning» 6(OOPSLA2), pp. 179:1526–179:1555, 2022
DOI: 10.1145/3563342
bibtex
J. Jakubovic, T. Petříček:
Ascending the ladder to self-sustainability, in To appear in Onward! 2022: Proceedings of the 2022 ACM SIGPLAN international symposium on new ideas, new paradigms, and reflections on programming and software, Auckland, New Zealand, December, 2022, 2022
Link bibtex
O. Flückiger, J. Ječmen, S. Krynski, J. Vitek:
Deoptless: speculation with dispatched on-stack replacement and specialized continuations, in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 749–761, 2022
ISBN: 978-1-4503-9265-5, DOI: 10.1145/3519939.3523729
Link bibtex
J. Brachthäuser, P. Schuster, E. Lee, A. Boruch-Gruszecki:
Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back, in Artifact of the paper "Effects, Capabilities, and Boxes: From Scope-based Reasoning to Type-based Reasoning and Back" 6(OOPSLA1), pp. 76:1–76:30, 2022
DOI: 10.1145/3527320
Link bibtex
J. Edwards, T. Petříček:
Interaction vs. Abstraction: Managed Copy and Paste, in Proceedings of the 1st ACM SIGPLAN International Workshop on Programming Abstractions and Interactive Notations, Tools, and Environments, pp. 11–19, 2022
ISBN: 978-1-4503-9910-4, DOI: 10.1145/3563836.3568723
Link bibtex
R. Perera, M. Nguyen, T. Petříček, M. Wang:
Linked visualisations via Galois dependencies, in Proceedings of the ACM on Programming Languages 6(POPL), pp. 7:1–7:29, 2022
DOI: 10.1145/3498668
Link bibtex
A. Turcotte, P. Donat-Bouillud, F. Křikava, J. Vitek:
signatr: A Data-Driven Fuzzing Tool for R, in Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, pp. 216–221, 2022
ISBN: 978-1-4503-9919-7, DOI: 10.1145/3567512.3567530
Link bibtex
T. Petříček:
The Gamma: Programmatic Data Exploration for Non-programmers, in 2022 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC), pp. 1-7, 2022
DOI: 10.1109/VL/HCC53370.2022.9833134