Functional Languages

UniPD
Completed

This project was developed as part of the Functional Languages course at the University of Padua. It consists of a collection of formal exercises and proofs covering the theoretical foundations of programming languages, with a particular focus on functional programming and λ-calculus.

The work explores topics such as:

Operational semantics and abstract machine execution
Inductive and rule-based proof techniques
Transition systems and program evaluation
Semantic equivalence of programs
Recursive definitions and fixed-point semantics
Type systems and subject reduction
Call-by-name and call-by-value evaluation strategies
Formal verification of language properties and correctness proofs

Through rigorous mathematical reasoning, the project demonstrates how programming language behavior can be formally specified, analyzed, and proven correct. The goal is to develop a deeper understanding of language design, program execution, and the theoretical principles that underpin modern functional programming languages.

To download the document: FunctionalLanguages.pdf

For the GitHub repository: Functional Languages