Browsing Theses by Supervisor "Lhoták, Ondřej"
Now showing items 1-11 of 11
-
Adding Reference Immutability to Scala
(University of Waterloo, 2023-07-10)Scala is a multi-paradigm programming language combining the power of functional and object-oriented programming. While Scala has many features promoting immutability, it lacks a built-in mechanism for controlling and ... -
Decidability and Algorithmic Analysis of Dependent Object Types (DOT)
(University of Waterloo, 2019-08-28)Dependent Object Types, or DOT, is a family of calculi developed to study the Scala programming language. These calculi have path dependent types as a feature, and potentially intersection types, union types and recursive ... -
Design and Implementation of Family Polymorphism for Interactive Theorem Proving
(University of Waterloo, 2023-06-13)With the growing practice of mechanizing language metatheories, it has become ever more pressing that interactive theorem provers make it easy to write reusable, extensible code and proofs. This thesis presents a novel ... -
Efficient Implementation of Parametric Polymorphism using Reified Types
(University of Waterloo, 2023-04-28)Parametric polymorphism is a language feature that lets programmers define code that behaves independently of the types of values it operates on. Using parametric polymorphism enables code reuse and improves the maintainability ... -
Efficient Pointer Analysis of Java in Logic
(University of Waterloo, 2017-05-16)Points-to analysis for Java benefits greatly from context sensitivity. CFL-reachability and k-limited context strings are two approaches to obtaining context sensitivity with different advantages: CFL-reachability ... -
Gradual Pluggable Typing in Java
(University of Waterloo, 2016-04-27)Gradual typing provides the ability to safely mix untyped or dynamically typed code with statically typed code while maintaining, within the statically typed portion, the guarantees claimed by the static typing. It is ... -
Implementing a Functional Language for Flix
(University of Waterloo, 2016-09-15)Static program analysis is a powerful technique for maintaining software, with applications such as compiler optimizations, code refactoring, and bug finding. Static analyzers are typically implemented in general-purpose ... -
A Path to DOT: Formalizing Scala with Dependent Object Types
(University of Waterloo, 2019-12-13)The goal of my thesis is to enable formal reasoning about the Scala programming language. To that end I present a core calculus that formalizes Scala's i) essential features in a ii) type-safe way and is iii) easy to extend ... -
Scala with Explicit Nulls
(University of Waterloo, 2019-12-20)The Scala programming language unifies the object-oriented and functional styles of programming. One common source of errors in Scala programs is null references. In this dissertation, I present a modification to the Scala ... -
TreeGen: a monotonically impure functional language
(University of Waterloo, 2020-08-19)We present TreeGen, an impure functional language designed to express, consume, and validate JSON-like documents, as well as generate text files. The language aims to provide a more reliable and flexible way to create ... -
κDOT: A DOT Calculus with Mutation and Constructors
(University of Waterloo, 2018-09-26)Scala is a functional and object-oriented programming language which unifies concepts from object and module systems by allowing for objects with type members which are referenced via path-dependent types. The Dependent ...