Fall 2026
Course Information & Syllabus
Instructor: Raj Sunderraman
Lectures: 12:30 PM – 2:15 PM (Mondays, Wednesdays) | Atlanta Campus | CLSO 306
Office: 1 Park Place, #629
Office Hours: MW 2:30 PM – 4:00 PM, or by appointment
E-mail: rsunderraman@gsu.edu
This
course explores the theoretical foundations and practical applications of
functional programming and advanced type systems. Bridging the formal logic
traditionally encountered in principles of computer science and automata theory
with modern software design, students will journey from the absolute primitives
of computation in the untyped and simply typed lambda calculus to robust,
effectful programming in Haskell. Through hands-on projects, students will
master core functional abstractions—including functors, applicatives, and
monads—while practically implementing foundational type-checking and inference
algorithms. The curriculum culminates in type-driven development using Idris 2,
where students will leverage dependent types and the Curry-Howard
correspondence to encode complex program invariants, ultimately constructing
provably correct systems such as a strictly verified relational algebra engine.
By the end of the term, students will possess both the rigorous mathematical
framework and the practical coding expertise required to design highly
expressive, safe, and verifiable software systems.
Module
1: Theoretical Foundations
· Untyped
Lambda Calculus: Syntax, free and bound variables, alpha-equivalence, and
beta-reduction.
· Church
Encodings: Representing Booleans, numerals, and standard data structures purely
through functions.
· Simply
Typed Lambda Calculus (STLC): Adding base types and function types; typing
rules and derivation trees; the concepts of progress and preservation.
Module
2: Applied Functional Programming (Haskell)
· Haskell
Basics: Syntax, lazy evaluation, basic types, and referential transparency.
· Data
Structures and Control Flow: Algebraic Data Types (ADTs), pattern matching,
recursion, and list comprehensions.
· Higher-Order
Functions: Map, fold, filter, and function composition.
· Polymorphism
& Type Classes: Ad-hoc polymorphism, defining and instantiating custom type
classes.
Module
3: Abstractions and Effects (Haskell)
· The
Typeclass Hierarchy: Deep dive into Functors and Applicatives.
· Monads
and the do Notation: Understanding the Monad laws and chaining computations.
· Managing
Effects: Programming with specific monads (Maybe, Either, State) and composing
pure code with IO.
Module
4: Dependent Types and Theorem Proving (Idris 2)
· Introduction
to Type-Driven Development: First-class types and the syntax of Idris 2.
· Dependent
Data Structures: Vectors with length encoded in the type; refined types.
· Propositions
as Types (Curry-Howard Correspondence): Writing proofs as functional programs;
equality types.
· State
and Effects in Idris: Encoding stateful protocols and transitions safely within
the type system.
Module
5: Type Checking and Inference (Bridging Theory and Practice) – If time
permits
· Algorithmic
Type Checking: Translating typing rules into a structural type-checking
algorithm for STLC.
· Type
Inference Basics: Unification, constraint generation, and the foundations of
the Hindley-Milner (Algorithm W) inference system.
·
Analyze and Evaluate Formal Systems: Formally reason about
computation by evaluating expressions and constructing proofs in both untyped
and simply typed lambda calculus.
·
Design Idiomatic Functional Software: Develop robust, purely
functional programs in Haskell, utilizing algebraic data types, pattern
matching, and higher-order functions.
·
Master Effectful Programming: Apply advanced functional
abstractions—specifically functors, applicatives, and monads—to cleanly manage
state, I/O, and side effects within a pure language.
·
Implement Foundational Type Systems: Construct basic type
checkers and implement type inference algorithms (e.g., Hindley-Milner) for
simple functional languages.
·
Apply Type-Driven Development: Leverage dependent types in Idris
2 to encode complex program invariants (such as propositions as types) and
construct provably correct software.
|
Item |
% of
Final grade |
|
Homework
Assignments |
30% |
|
Exam 1
(in class) |
25% |
|
Exam 2
(in class) |
25% |
|
Project |
20% |
At the end of the course, your weighted numerical average will be
converted into letter grades based on the following scale. The plus/minus
system is applied (see https://registrar.gsu.edu/academic-records/grading/#gpa).
|
Percentage |
Grade
range |
|
90 to 100% |
A
(A- starts at 90%, A starts at 93%, A+ starts at 97%) |
|
80%
to <90% |
B
(B- starts at 80%, B starts at 83%, B+ starts at 87%) |
|
70%
to <80% |
C |
|
60%
to <70% |
D |
|
0%
to <60% |
F |
All work, including homework/programming
assignments and exams, must be your individual work. You may not work with
other students on shared solutions. Specifically, you must never copy someone
else’s solution or code. If you are having trouble with an assignment, please
consult with me. You may discuss problems and solution approaches with other
students, but submitting code or other solutions as your own work that you
cannot explain or reproduce in a controlled environment is considered academic
dishonesty.
Course Philosophy on Generative AI. For the
first time, this course will introduce you to the cutting-edge world of
Generative AI. We are actively piloting the use of these tools in this lab to
give you a flavor for what Generative AI is capable of and how it can be used
to improve programming productivity. You will learn how to use these powerful
techniques to assist in code generation, giving you a competitive edge in your
future.
However, Generative AI is a tool to assist your
learning, not to replace it. Our primary objective is for you to build a
strong, independent understanding of fundamental computational principles. We
do not want to diminish our learning of the subject matter with the
over-reliance on Generative AI.
Guidelines for Use
To ensure you are truly mastering the material,
please adhere to the following guidelines:
·
Minimize Reliance: While you are permitted to
explore Generative AI for your programming assignments, it is highly
recommended that you use it—and any other outside assistance—as little as
possible.
·
Total Comprehension is Required: If you use AI
to generate or debug a portion of your code, you are fully responsible for
understanding exactly how and why that code works.
·
Oral Examinations. Your understanding will be
directly assessed. For these specific assignments, you will participate in a
15-minute oral examination in my office. You must be able to clearly answer
questions about your submission and explain the underlying logic of your code.
·
Strictly Prohibited During Exams: The two exams
are strictly closed assistance. You may not use Generative AI, external
websites, or any other form of outside assistance during these assessments.
Grading Impact
Please keep in mind that your independent
understanding of the underlying computational principles accounts for slightly
more than 50% of your total grade (comprising the two exams and randomly
selected oral examinations on homework and project). Misusing AI tools to
bypass the learning process will directly and negatively impact your ability to
succeed in these heavily weighted assessments.
Students are expected to attend all classes. Any material missed in class is up to students to make up on their own time. Attendance is critical as lectures will cover topics that will not be addressed in the homework assignments and may be asked in the exams.
I am committed to fostering an inclusive and supportive environment in this class, where diverse ideas and values are welcomed and recognized as essential for success. My goal is to ensure that all students, regardless of their backgrounds or perspectives, receive the support they need to excel in this course.
Active participation in class discussions is highly encouraged. As members of this learning community, students are expected to contribute thoughtfully, create an atmosphere that values inquiry and self-expression, and demonstrate a sincere effort to understand and respect the diverse perspectives, backgrounds, and experiences of their peers. Disruptive classroom behavior will not be tolerated.
“Students who wish to request an accommodation for a disability may do so by registering with the Access and Accommodation Center. Students may only be accommodated upon issuance by the Access and Accommodation Center (https://access.gsu.edu/) of a signed Accommodation Plan and are responsible for providing a copy of that plan to instructors of all classes in which accommodations are sought.” Students are encouraged to contact the instructor early in the semester to discuss accommodation needs.
“Your constructive assessment of this course is indispensable in shaping education at Georgia State. Upon completing the course, please take the time to fill out the online course evaluation.”
“The course syllabus provides a general plan for the course; however, deviations may be necessary.”