Programming Languages Winter School 2026
7–11 December 2026 SSB 334, IIT Madras
This five-day school introduces programming languages, program verification, and runtime systems through lectures and exercises.
Apply to attend: Applications will open soon. We will review your application and let you know whether you have a seat. Travel and accommodation support will be available for those who need it.
Audience
The school welcomes senior undergraduates, graduate students, research staff, faculty, and industry professionals in research positions. Prior study of programming languages, functional programming, or proof assistants is not required.
Programming experience and discrete mathematics are the core foundations for the school. Theory of computation or a Logic for Mathematics and Computer Science (LMC) course is strongly recommended. Data structures and algorithms are useful preparation. Compilers and operating systems are helpful additional background, but are not required.
The discrete mathematics background should include logic and reading and writing basic proofs. Equivalent self-study or work experience is welcome.
Timetable
The timetable is provisional. All times are India Standard Time (UTC+5:30). Each lecture lasts 80 minutes, including questions.
Breaks: 10:20–10:40 and 15:20–15:40. Lunch: 12:00–14:00.
Modules
Further abstracts and preparation details will be added as they are confirmed.
Rocq & Roll
Aalok Thakkar (Ashoka University) and TVH Prathamesh (Krea University)
This course introduces Rocq, an interactive theorem prover used to formally specify and verify the correctness of logical statements and programs. Starting with basic definitions, inductive types, and proofs, we will gradually build up to formalizing the Simply Typed Lambda Calculus. Along the way, you will gain hands-on experience writing definitions and constructing machine-checked proofs using the SSReflect proof language.
- Introduction to Rocq: basic definitions, functions, and proofs
- Inductive types, recursive functions, and proofs by induction
- Simply Typed Lambda Calculus (STLC) in Rocq
- Proving progress, preservation, and type safety of STLC
Familiarity with introductory logic, including propositional and first-order predicate logic, is recommended. A preparatory handout will be shared with participants.
Bring a laptop with Rocq 9.0 and the stdpp library installed. Participants without a laptop are welcome to pair up during the hands-on sessions. See the Rocq installation instructions.
Further reading:
Design of Type Systems
Suresh Jagannathan (Purdue University)
Robin Milner’s famous quote, “Well-typed programs don’t go wrong” speaks to the centrality of types in modern programming. In this module, we will explore the design of type systems from both a foundational and practical perspective. We will bridge abstract logical principles with the mechanics underlying the design and implementation of type systems in real-world languages. The lectures will cover (a) the relationship between types and formal logic, typing judgements, and safety; (b) polymorphism and generics; (c) types and resource management as exemplified in languages like Rust, and (d) refinement types and its various extensions that allow types to carry logical predicates enabling richer and more expressive program reasoning and verification capabilities.
- Judgements, Propositions, Curry-Howard, and STLC
- Polymorphism (System F, subtyping, row)
- Substructural Type Systems, Rust
- Refinement Types and Extensions
No labs are scheduled, and no software installation is required. Recent versions of OCaml and Z3 are optional for participants who would like to try the demonstrations.
Symbolic Verification of Security Protocols
Vaishnavi Sundararajan (IIT Delhi)
Symbolic approaches to verifying security protocols, with take-home exercises between the first and second day.
The planned exercises do not require Tamarin or ProVerif.
Concurrent Separation Logic
S P Suresh (Chennai Mathematical Institute)
An introduction to concurrent separation logic, with examples and a glimpse of Iris.
eBPF and Abstract Interpretation
Srinivas Narayana (IIT Madras)
Abstract to follow.
Runtime Systems and JIT Compilation
Manas Thakur (IIT Bombay)
Just-in-time (JIT) compilers offer novel ways to optimize programs based on their execution profile and have found significant usage in languages with managed runtimes. However, as JIT compilation directly affects the execution time of a program, precision-enhancement techniques from the static-analysis world seldom find way into these otherwise powerful systems. Under this backdrop, we would first understand how modern JIT compilers optimize code, in tiered runtime systems, using examples of program analysis aimed at enabling stack allocation of heap objects in Java. We would then understand techniques to not only allocate a large number of objects on stack (leading to reduced garbage collection and improved performance), but to also handle challenges posed by possible dynamism in real-world Java Virtual Machines. In particular, we would talk about AOT-analysis guided optimistic stack allocation, as well as the usage of speculative JIT information in improving the precision of statically computed results. All parts of the story would be bound by the over-arching goal of maintaining precision and efficiency, while being sound, during program execution.
Install OpenJDK on your laptop. Any version is suitable for this module.
Contact: contact@fplaunchpad.org