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

Postdoc
Type Systems, Knowledge Management, AI
Postdoc
Graphical Constraint Programming for Notational Freedom
Assistant professor
Programming Systems and Languages, History and Philosophy of Computing
Ph.D. student
Functional Programming, Type Systems
Ph.D. student
Proof Assistants, Type Systems, Programming Systems and Languages
Professor
Programming Systems and Languages

Recent Publications

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
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
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
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
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
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
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
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
J. Edwards, T. Petříček, T. van der Storm:
Live & Local Schema Change: Challenge Problems, in , 2023
DOI: 10.48550/arXiv.2309.11406
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
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
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
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
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
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
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
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
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
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