Polymorphism and Proofs

This lecture covers parametric polymorphism, lists construction, tuples, generic methods, merge sort, proving program properties, higher-order list functions, subtyping, generics, type parameters, generic functions, type inference, and exercises with generics. It also delves into Scala lists, constructors of lists, right associativity, operations on lists, decomposing lists using patterns, sorting lists, insertion sort, merge sort, tuples, and generic methods. The lecture emphasizes the importance of structural induction, referential transparency, laws of concatenation, and reduction of lists using functions like map, filter, reduceLeft, foldLeft, reduceRight, and foldRight.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related lectures (200)

Related concepts (192)

Standard ML

Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers. Standard ML is a modern dialect of ML, the language used in the Logic for Computable Functions (LCF) theorem-proving project. It is distinctive among widely used languages in that it has a formal specification, given as typing rules and operational semantics in The Definition of Standard ML.

Rust (programming language)

Rust is a multi-paradigm, general-purpose programming language that emphasizes performance, type safety, and concurrency. It enforces memory safety—ensuring that all references point to valid memory—without requiring the use of a garbage collector or reference counting present in other memory-safe languages. To simultaneously enforce memory safety and prevent data races, its "borrow checker" tracks the object lifetime of all references in a program during compilation.

Mathematical proof

A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems; but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning which establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning which establish "reasonable expectation".

Polymorphism (biology)

In biology, polymorphism is the occurrence of two or more clearly different morphs or forms, also referred to as alternative phenotypes, in the population of a species. To be classified as such, morphs must occupy the same habitat at the same time and belong to a panmictic population (one with random mating). Put simply, polymorphism is when there are two or more possibilities of a trait on a gene. For example, there is more than one possible trait in terms of a jaguar's skin colouring; they can be light morph or dark morph.

Linked list

In computer science, a linked list is a linear collection of data elements whose order is not given by their physical placement in memory. Instead, each element points to the next. It is a data structure consisting of a collection of nodes which together represent a sequence. In its most basic form, each node contains data, and a reference (in other words, a link) to the next node in the sequence. This structure allows for efficient insertion or removal of elements from any position in the sequence during iteration.

Class hierarchies: pattern matching

Covers class hierarchies, pattern matching, function values, and function calls in Scala.

Contextual Abstraction

Explores contextual abstraction in software construction, discussing how functions and classes can be written without detailed knowledge of the context in which they will be used.

Code Generation Lab CS-320: Computer language processing

Covers generating code for a compiler, translating an Amy program to WebAssembly, including memory management and pattern matching compilation.

Class Hierarchies: Pattern Matching

Explores class hierarchies, case classes, enums, pattern matching, and function values in Scala.

Recursive Algorithms: Induction & Sorting CS-101: Advanced information, computation, communication I

Explores induction, recursion, and sorting algorithms, including merge sort and the proof of correctness for recursive algorithms.