Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Safe Mutation in Practice

In course

CS-214: Software construction

Learn how to design and implement reliable, maintainable, and efficient software using a mix of programming skills (declarative style, higher-order functions, inductive types, parallelism) and fundamental software construction concepts (reusability, abstr ...

Description

This lecture covers the implementation of safe mutation in functional programming, focusing on lazy evaluation, lazy cells, object invariants, and caching functions. It discusses the Floyd-Marshall algorithm and the correctness theorem for lazy cells. The instructor explains the challenges of breaking lazy cell results and types, and provides solutions to ensure safety and efficiency. The lecture also explores memoization techniques, cached functions, and dynamic programming for optimizing recursive functions.

Instructors (2)

Martin Odersky

Martin Odersky heads the programming research group at EPFL. His research interests cover fundamental as well as applied aspects of programming languages. They include semantics, type systems, programming language design, and compiler construction. The main focus if his work lies in the integration of object-oriented and functional programming. His research thesis is that the two paradigms are just two sides of the same coin and should be unified as much as possible. To prove this he has experimented a number of language designs, from Pizza to GJ to Functional Nets. He has also influenced the development of Java as a co-designer of Java generics and as the original author of the current javac reference compiler. His current work concentrates on the Scala programming language, which unifies FP and OOP, while staying completely interoperable with Java and .NET. Martin Odersky got his doctorate from ETHZ, in 1989. He held research positions at the IBM T.J. Watson Research Center from 1989 and at Yale University from 1991. He was then a professor at the University of Karlsruhe from 1993 and at the University of South Australia from 1997. He joined EPFL as full professor in 1999. He is associate editor of the Journal of Functional Programming and member of IFIP WG 2.8. He was conference chair for ICFP 2000, and program chair for ECOOP 2004 as well as ETAPS/CC 2007.

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Official source

Ontological neighbourhood

Theoretical computer science

Programming language theory: High-level programming languages

Related concepts (32)

Lazy evaluation

In programming language theory, lazy evaluation, or call-by-need, is an evaluation strategy which delays the evaluation of an expression until its value is needed (non-strict evaluation) and which also avoids repeated evaluations (by the use of sharing). The benefits of lazy evaluation include: The ability to define control flow (structures) as abstractions instead of primitives. The ability to define potentially infinite data structures. This allows for more straightforward implementation of some algorithms.

Memoization

In computing, memoization or memoisation is an optimization technique used primarily to speed up computer programs by storing the results of expensive function calls to pure functions and returning the cached result when the same inputs occur again. Memoization has also been used in other contexts (and for purposes other than speed gains), such as in simple mutually recursive descent parsing. It is a type of caching, distinct from other forms of caching such as buffering and page replacement.

Functional programming

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program. In functional programming, functions are treated as first-class citizens, meaning that they can be bound to names (including local identifiers), passed as arguments, and returned from other functions, just as any other data type can.

Evaluation strategy

In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a parameter-passing strategy that defines the kind of value that is passed to the function for each parameter (the binding strategy) and whether to evaluate the parameters of a function call, and if so in what order (the evaluation order). The notion of reduction strategy is distinct, although some authors conflate the two terms and the definition of each term is not widely agreed upon.

Cache (computing)

In computing, a cache (kæʃ ) is a hardware or software component that stores data so that future requests for that data can be served faster; the data stored in a cache might be the result of an earlier computation or a copy of data stored elsewhere. A cache hit occurs when the requested data can be found in a cache, while a cache miss occurs when it cannot. Cache hits are served by reading data from the cache, which is faster than recomputing a result or reading from a slower data store; thus, the more requests that can be served from the cache, the faster the system performs.

Related lectures (41)

Lazy Evaluation: Lazy Lists

Explores lazy evaluation and lazy lists in Scala, emphasizing their benefits and implementation.

Verifying Programs with Stainless: Part 2

Focuses on using Stainless for program verification, demonstrating the process of verifying programs and ensuring correctness.

Stainless Verification System Tutorial

Introduces Stainless, an open-source tool for verifying Scala programs, covering language, modeling, verification tips, and inner workings.

Functional Programming Basics in Scala

Covers the basics of functional programming in Scala, including evaluation strategies, conditionals, and value definitions, with a focus on computing square roots with Newton's method.

Recursive Functions: Substitution Interpreter