\( % Latex Preamble definitions here (mostly usepackage) \usepackage% %[dvipsnames] {xcolor} % make sure this is before the loading font packages \newcommand\hmmax{0} \newcommand\bmmax{0} \usepackage{amssymb} \usepackage{amsmath} \usepackage{mathtools} \usepackage %[dvipsnames] {graphicx} \usepackage{float} %\usepackage[numbers]{natbib} \usepackage[document]{ragged2e} % % enumitem doesn't seem to work with beamer %\usepackage[inline]{enumitem} \usepackage{wrapfig} \usepackage{stackrel} % extensible arrows \usepackage{extpfeil} % \usepackage{trfrac} \usepackage{amsthm} \usepackage{tikz} \usepackage{tikz-cd} \usepackage{tikz} \usepackage{tikz-qtree} \usetikzlibrary{automata, positioning, arrows, shapes.geometric} \usepackage{turnstile} \usepackage{comment} %https://tex.stackexchange.com/questions/21334/is-there-a-package-that-has-the-clockwise-gapped-circle-arrow-in-it % \usepackage{mathbx} \usepackage{datetime} \usepackage{datetime2} %% Also See %% http://u.cs.biu.ac.il/~tsaban/Pdf/LaTeXCommonErrs.pdf %% for general tips \usepackage{listings} \usepackage{subfigure} \usepackage{bm} \usepackage{amsfonts} %% - also included by amssymb \usepackage{mathpazo} %% - because the OP uses mathpazo, optional %\usepackage{tufte-latex} \usepackage{comment} \usepackage{mathtools} \usepackage{bussproofs} \usepackage{hyperref} %\usepackage{cleveref} \)
\( %% Your math definitions here % \newcommand{\alphaequiv}{{\underset{\raise 0.7em\alpha}{=}}} \newcommand{\yields}{\Rightarrow} \newcommand{\derives}{\overset{*}{\yields}} \newcommand{\alphaequiv}{=_{\alpha}} \newcommand{\tto}[2]{{\overset{#1}{\underset{#2}{\longrightarrow}}}} \newcommand{\transitsto}[2]{{\overset{#1}{\underset{#2}{\longrightarrow}}}} \newcommand{\xtransitsto}[2]{{\underset{#2}{\xrightarrow{#1}}}} \newcommand{\xtransitsfrom}[2]{{\underset{#2}{\xleftarrow{#1}}}} \newcommand{\xto}[2]{{\xtransitsto{#1}{#2}}} \newcommand{\xfrom}[2]{{\xtransitsfrom{#1}{#2}}} \newcommand{\xreaches}[2]{{\underset{#2}{\xtwoheadrightarrow{#1}}}} \newcommand{\reaches}[2]{{\underset{#2}{\xtwoheadrightarrow{#1}}}} %\newcommand{\reaches}[2]{{\overset{#1}{\underset{#2}{\twoheadrightarrow}}}} %\newcommand{\goesto}[2]{\transitsto{#1}{#2}} %\newcommand{\betareducesto}{{\underset{\beta}{\rightarrow}}} \newcommand{\betareducesto}{\rightarrow_{\beta}} %\newcommand{\etareducesto}{{\underset{\eta}{\rightarrow}}} \newcommand{\etareducesto}{\rightarrow_{\eta}} %\newcommand{\betaetareducesto}{{\underset{\beta\ \eta}{\rightarrow}}} \newcommand{\betaetareducesto}{\rightarrow_{\beta\eta}} \newcommand{\preducesto}{\rhd} \newcommand{\psimplifiesto}{\stackrel{\scriptstyle{*}}{\rhd}} \newcommand{\lreducesto}{\rightsquigarrow} \newcommand{\lsimplifiesto}{\stackrel{\scriptstyle{*}}{\lreducesto}} \newcommand{\rewritesto}{\hookrightarrow} \newcommand{\goesto}[1]{\stackrel{#1}{\rightarrow}} \newcommand{\xgoesto}[1]{\xrightarrow{#1}} \newcommand{\reducesto}{\stackrel{}{\rightarrow}} \newcommand{\simplifiesto}{\stackrel{\scriptstyle{*}}{\rightarrow}} \newcommand{\connected}[1]{\stackrel{#1}{\leftrightarrow}} \newcommand{\joins}{\downarrow} \newcommand{\evaluatesto}{\Longrightarrow} %\newcommand{\lit}[1]{\hbox{\sf{#1}}} \newcommand{\lit}[1]{{\sf{#1}}} \newcommand{\true}{\lit{true}} \newcommand{\false}{\lit{false}} \def\Z{\mbox{${\mathbb Z}$}} \def\N{\mbox{${\mathbb N}$}} \def\P{\mbox{${\mathbb P}$}} \def\R{\mbox{${\mathbb R}$}} \def\T{\mbox{${\mathbb T}$}} \newcommand{\Rp}{{\mathbb{R}}^+} \def\Bool{\mbox{${\mathbb B}$}} \def\Q{\mbox{${\mathbb Q}$}} \def\sA{\mbox{${\cal A}$}} \def\sB{\mbox{${\cal B}$}} \def\sC{\mbox{${\cal C}$}} \def\sD{\mbox{${\cal D}$}} \def\sF{\mbox{${\cal F}$}} \def\sG{\mbox{${\cal G}$}} \def\sL{\mbox{${\cal L}$}} \def\sP{\mbox{${\cal P}$}} \def\sM{\mbox{${\cal M}$}} \def\sN{\mbox{${\cal N}$}} \def\sR{\mbox{${\cal R}$}} \def\sS{\mbox{${\cal S}$}} \def\sO{\mbox{${\cal O}$}} \def\sT{\mbox{${\cal T}$}} \def\sU{\mbox{${\cal U}$}} \def\th{\mbox{$\widetilde{h}$}} \def\tg{\mbox{$\widetilde{g}$}} \def\tP{\mbox{$\widetilde{P}$}} \def\norm{\mbox{$\parallel$}} \def\osum{${{\bigcirc}}\!\!\!\!{\rm s}~$} \def\pf{\noindent {\bf Proof}~~} \def\exec{\mathit{exec}} \def\Act{\mathit{A\!ct}} \def\Traces{\mathit{Traces}} \def\Spec{\mathit{Spec}} \def\uns{\mathit{unless}} \def\ens{\mathit{ensures}} \def\lto{\mathit{leads\!\!-\!\!to}} \def\a{\alpha} \def\b{\beta} \def\c{\gamma} \def\d{\delta} \def\sP{\mbox{${\cal P}$}} \def\sM{\mbox{${\cal M}$}} \def\sA{\mbox{${\cal A}$}} \def\sB{\mbox{${\cal B}$}} \def\sC{\mbox{${\cal C}$}} \def\sI{\mbox{${\cal I}$}} \def\sS{\mbox{${\cal S}$}} \def\sD{\mbox{${\cal D}$}} \def\sF{\mbox{${\cal F}$}} \def\sG{\mbox{${\cal G}$}} \def\sR{\mbox{${\cal R}$}} \def\tg{\mbox{$\widetilde{g}$}} \def\ta{\mbox{$\widetilde{a}$}} \def\tb{\mbox{$\widetilde{b}$}} \def\tc{\mbox{$\widetilde{c}$}} \def\tx{\mbox{$\widetilde{x}$}} \def\ty{\mbox{$\widetilde{y}$}} \def\tz{\mbox{$\widetilde{z}$}} \def\tI{\mbox{$\widetilde{I}$}} \def\norm{\mbox{$\parallel$}} \def\sL{\mbox{${\cal L}$}} \def\sM{\mbox{${\cal M}$}} \def\sN{\mbox{${\cal N}$}} \def\th{\mbox{$\widetilde{h}$}} \def\tg{\mbox{$\widetilde{g}$}} \def\tP{\mbox{$\widetilde{P}$}} \def\norm{\mbox{$\parallel$}} \def\to{\rightarrow} \def\ov{\overline} \def\gets{\leftarrow} \def\too{\longrightarrow} \def\To{\Rightarrow} %\def\points{\mapsto} %\def\yields{\mapsto^{*}} \def\un{\underline} \def\vep{$\varepsilon$} \def\ep{$\epsilon$} \def\tri{$\bigtriangleup$} \def\Fi{$F^{\infty}$} \def\Di{\Delta^{\infty}} \def\ebox\Box \def\emp{\emptyset} \def\leadsto{\rightharpoondown^{*}} \newcommand{\benum}{\begin{enumerate}} \newcommand{\eenum}{\end{enumerate}} \newcommand{\bdes}{\begin{description}} \newcommand{\edes}{\end{description}} \newcommand{\bt}{\begin{theorem}} \newcommand{\et}{\end{theorem}} \newcommand{\bl}{\begin{lemma}} \newcommand{\el}{\end{lemma}} % \newcommand{\bp}{\begin{prop}} % \newcommand{\ep}{\end{prop}} \newcommand{\bd}{\begin{defn}} \newcommand{\ed}{\end{defn}} \newcommand{\brem}{\begin{remark}} \newcommand{\erem}{\end{remark}} \newcommand{\bxr}{\begin{exercise}} \newcommand{\exr}{\end{exercise}} \newcommand{\bxm}{\begin{example}} \newcommand{\exm}{\end{example}} \newcommand{\beqa}{\begin{eqnarray*}} \newcommand{\eeqa}{\end{eqnarray*}} \newcommand{\bc}{\begin{center}} \newcommand{\ec}{\end{center}} \newcommand{\bcent}{\begin{center}} \newcommand{\ecent}{\end{center}} \newcommand{\la}{\langle} \newcommand{\ra}{\rangle} \newcommand{\bcor}{\begin{corollary}} \newcommand{\ecor}{\end{corollary}} \newcommand{\bds}{\begin{defns}} \newcommand{\eds}{\end{defns}} \newcommand{\brems}{\begin{remarks}} \newcommand{\erems}{\end{remarks}} \newcommand{\bxrs}{\begin{exercises}} \newcommand{\exrs}{\end{exercises}} \newcommand{\bxms}{\begin{examples}} \newcommand{\exms}{\end{examples}} \newcommand{\bfig}{\begin{figure}} \newcommand{\efig}{\end{figure}} \newcommand{\set}[1]{\{#1\}} \newcommand{\pair}[1]{\langle #1\rangle} \newcommand{\tuple}[1]{\langle #1\rangle} \newcommand{\size}[1]{| #1 |} \newcommand{\union}{\cup} \newcommand{\Union}{\bigcup} \newcommand{\intersection}{\cap} \newcommand{\Intersection}{\bigcap} \newcommand{\B}{\textbf{B}} %\newcommand{\be}[2]{\begin{equation} \label{#1} \tag{#2} \end{equation}} \newcommand{\abs}[1]{{\lvert}#1{\rvert}} \newcommand{\id}[1]{\mathit{#1}} \newcommand{\pfun}{\rightharpoonup} %\newcommand{\ra}[1]{\kern-1.5ex\xrightarrow{\ \ #1\ \ }\phantom{}\kern-1.5ex} %\newcommand{\ras}[1]{\kern-1.5ex\xrightarrow{\ \ \smash{#1}\ \ }\phantom{}\kern-1.5ex} \newcommand{\da}[1]{\bigg\downarrow\raise.5ex\rlap{\scriptstyle#1}} \newcommand{\ua}[1]{\bigg\uparrow\raise.5ex\rlap{\scriptstyle#1}} % \newcommand{\lift}[1]{#1_{\bot}} \newcommand{\signal}[1]{\tilde{#1}} \newcommand{\ida}{\stackrel{{\sf def}}{=}} \newcommand{\eqn}{\doteq} \newcommand{\deduce}[1]{\sststile{#1}{}} %% These don't sit very well with MathJax %% so we don't plan to use theorem like environments %% in org documents. %% instead we plan to use headings with %% 1. property drawers with a CLASS property identifying %% the environment %% 2. A tag with the same name as the CLASS property %% In LaTeX export, these turn into (sub)sections. %% See http://u.cs.biu.ac.il/~tsaban/Pdf/LaTeXCommonErrs.pdf %% \newtheorem{prop}[thm]{Proposition} %% \theoremstyle{plain}%default %% \newtheorem{theorem}{Theorem}[section] %% \newtheorem{lemma}{Lemma}[section] %% \newtheorem{corollary}{Corollary}[section] %% \newtheorem{definition}{Definition}[section] %% \newtheorem{remark}{Remark}[section] %% \newtheorem{example}{Example}[section] %% \newtheorem{exercise}{Exercise}[section] \newcommand{\less}[1]{#1_{<}} \newcommand{\pfn}{\rightharpoonup} \newcommand{\ffn}{\stackrel{{\sf fin}}{\rightharpoonup}} \newcommand{\stkout}[1]{\ifmmode\text{\sout{\ensuremath{#1}}}\else\sout{#1}\fi} % Caution: Not supported by MathJax! % ---------------------------------- % \DeclareMathSymbol{\shortminus}{\mathbin}{AMSa}{"39} % \usepackage{amsfonts} %% <- also included by amssymb % \DeclareMathSymbol{\shortminus}{\mathbin}{AMSa}{"39} \usepackage{mathpazo} %% <- because the OP uses mathpazo, optional \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\floor}[1]{\left\lfloor #1 \right\rfloor} \newcommand{\ceil}[1]{\left\lceil #1 \right\rceil} \newcommand{\rel}{\twoheadrightarrow} \newcommand{\map}{\rightarrow} %\newcommand{\fixed}{\boldsymbol{\circlearrowleft}} \newcommand{\terminal}{\not\xto{}{}} \newcommand{\fixed}{\bm\circlearrowleft} \newcommand{\imp}{\rightarrow} \newcommand{\dimp}{\leftrightarrow} % double implication \newcommand{\lequiv}{\Longleftrightarrow} % logical equivalence \newcommand{\limplies}{\Rightarrow} \newcommand{\lxor}{\veebar} \)
UP | HOME

PoPL 2023-Monsoon @ IIITH

Table of Contents

1 Course Info

Number
CSC 415
Name
Principles of Programming Languages (PoPL)
Lectures
Himalaya 102, Tue, Fri 2pm-3:25pm (India Standard Time UTC+5:30)
Instructor
  • Venkatesh Choppella <venkatesh.choppella@iiit.ac.in>
Teaching Assistants
Kunwar Shanjeet Singh Grover
Office Hours
  • Venkatesh: by appt. (Please email Sahiti Potnuru sahiti_potnuru123@gmail.com for appointments.)

2 Course infrastructure

Course web pages
https://iiit.ac.in/~vxc/popl
  • Homework submission on Gitlab:: You will need an account on https://www.gitlab.com. Your homeworks need to be committed in a private repository accessible only to you and the to the TAs and instructor. The exact directory structure will be specified by the TAs.
Source code
The Racket/Scheme source code for all the code in Essentials of Programming Languages 3rd Edition is available at https://github.com/mwand/eopl3.

3 Objectives, Prerequisites and Syllabus

Please see the course announcement page.

4 Texts and References

4.1 Main texts

EOPL
Essentials of Programming Languages 3rd Edition. Friedman and Wand. This is the main text for the course. Available on Amazon.in.
HtDP
How to Design Programs. Felleisen et al. Available online. Uses Racket exclusively.
TRaAT
Term Rewriting and All That. Baader and Nipkow. Chapters 1 and 2. Chapter copies on reserve in the library.

4.2 Related Texts

SICP
Structure and Interpretation of Programs. Abelson and Sussman. Available online. Accompanying video lectures also available online.
PLAI
Programming Languages: Application and Interpretation 2nd Edition. Shriram Krishnamurti. Available online.
SSICS
Simply Scheme: Introducing Computer Science. Brian Harvey and Matthew Wright. Available online.
RG
Racket Guide. Available as part of Racket language documentation.

5 Grading (tentative)

Item unit marks no. total Remarks
HW TBA TBA 15 Not all HWs may
        have equal weight
Quiz1     7.5  
Quiz2     7.5  
Mid     20  
Final     30  
Proj     20  
Total     100  

6 Academic integrity

6.1 Discussion and Collaboration

You are encouraged to discuss the course material and the homework and its solutions with your classmates. After consulting with your friends, however, you are expected to implement the homework solutions on your own. The TAs will be checking your commit history and examine your report for plagiarism or copying.

When answering a quiz, you are expected to not rely on any dishonest means like discussing with classmates or referring to online material.

When collaborating with your classmates in projects, please ensure that you properly credit your fellow contributors.

6.2 Penalties

Homeworks
If you are caught adopting unfair means in doing homeworks, you will receive a zero for that homework and all previous homeworks.
Quizzes
If you are caught adopting unfair means in a quiz, you will receive a zero for that quiz and all previous quizzes.
Project
If you adopt unfair means in your project, you will receive a zero for that project.

7 Lecture Plan

Lec No. Date Topic Reading Assignments Note Estimated
        taker Effort
1. [2023-08-01 Tue] Functional Programming with Racket Introduction to Racket    
      Racket Guide    
2. [2023-08-04 Fri] Higher-order functions, Functional Programming in Racket    
    pattern matching      
3. [2023-08-08 Tue] Transition Systems and Mapcode Notes on Mapcode    
4. [2023-08-11 Fri] Abstract Reduction Systems Notes, TRaat Sec 2 Shiven  
5. [2023-08-14 Mon] ARS properties, Address spaces Notes on Abstract Reductions Dheeraja  
6. [2023-08-18 Fri] Interactive Evaluation   Kriti  
7. [2023-08-22 Tue] Well-founded induction, Local confluence Notes on Abstract Reductions Bharat  
8. [2023-08-25 Fri] Operational Semantics: ADDITION & IF+DIV ADDITION IF+DIV Shamil  
9. [2023-08-29 Tue] Quiz 1      
  [2023-09-01 Fri] Class cancelled      
10. [2023-09-05 Tue] Evaluation Semantics ADDITION IF+DIV    
11. [2023-09-08 Fri] Lexical Scope, Environments EoPL Sec 3.1–3.2 Mayank  
12. [2023-09-09 Sat] Makeup classes: Closures and EoPL Sec 3.3    
    higher-order functions      
13. [2023-09-12 Tue] Closures (contd.) Scope and Extent EoPL Sec 3.3    
14. [2023-09-15 Fri] Recursion EoPL Sec 3.4    
  [2023-09-19 Tue] Holiday (Vinayaka Chaturthi)      
  [2023-09-22 Fri] MIDSEM WEEK      
15. [2023-10-03 Tue] Recursion and the Y combinator Notes    
16. [2023-10-06 Fri] Stores and Mutation EoPL Sec 4.1-4.3    
17. [2023-10-07 Sat] Makeup class: Notes    
    PARLANG: a small parallel language      
18. [2023-10-10 Tue] From closures to objects Notes    
19. [2023-10-13 Fri] Makeup class: Javascript    
    Embedding Javascript in Racket Safe programming in JS    
      JS objects in Racket    
      embedding JS in Racket    
      Basic Obj model in Scheme revisited    
20. [2023-10-17 Tue] Lambda Calculus 1: Syntax and substitution Notes    
21. [2023-10-20 Fri] Quiz 2      
22. [2023-10-27 Fri] Lambda Calculus 2: Reduction, parallel Notes    
    reduction and confluence      
23. [2023-10-31 Tue] Church Numerals Notes    
24. [2023-11-03 Fri] Imperative Form and Note on imperative form    
    Continuation Passing Style EoPL Sec 6.1    
25. [2023-11-07 Tue] Continuation Passing Interpreters EoPL Sec 5.1 and 5.2    
  [2023-11-10 Fri] No Class (Saturday Schedule) EoPL Sec 5.1 and 5.2    
26. [2023-11-14 Tue] Project Review session      
27. [2023-11-17 Fri] Transformation of representations EoPL Sec 5.3    
    of continuations: Factorial example Notes    
28. [2023-11-21 Tue] Exceptions and Letcc EoPL Sec 5.4    
      Notes on Exceptions and LETCC    
29. [2023-12-02 Sat 14:00] Final Project Presentation      
30. [2023-12-04 Mon] Project Final report submission      
    (process to be announced)      
31. [2023-12-04 Mon] Final Exam Paper showing      
    (Room to be announced)      
32. [2023-12-05 Tue] Grades submission to Academic Office      

8 License

Material in the POPL course pages is covered by the Creative Commons CC-BY-NC-ND Attribution-NonCommercial-NoDerivs license. You are free to use the material for non commercial purposes without changing it and after attribution.

Author: Venkatesh Choppella

Created: 2023-11-25 Sat 09:14

Validate