Programming Languages Delft

Welcome to @NathanielB@types.pl who has just started his PhD in our group!

Master thesis by Gideon Bot: "Rethinking Dependent Type Checking, Co-Contextually"

"This work explores a co-contextual formulation of a dependent type system and its accompanying type-checking algorithm. Both incremental and parallel variants of the algorithm are implemented for the dependently typed lambda calculus Elara, based on LambdaPi (Löh, McBride, and Swierstra, 2010)."

https://resolver.tudelft.nl/uuid:79e488af-6703-4558-b2c6-1606f8ba1f14

#Master #thesis #DependentTypes #Incremental #Concurrent #TypeChecking

Master thesis by Maria Khakimova: "Enhancing Proof Assistant Error Messages with Hints: A User Study"

"We implemented hint enhancements for the error messages displayed upon three common mistakes: forgetting whitespace, using confusable Unicode characters, and supplying too few arguments to a function. A between-participants user study was then conducted with 70 students [..]"

https://repository.tudelft.nl/record/uuid:52513287-7149-41f1-a8e8-8e38696cb283

#Agda #DependentTypes #ProofAssistants #ErrorMessages #Usability #UserStudy #master #thesis

Master thesis by Csanad Farkas:
"Formalisation of Display Map Categories in Univalent Foundations"

"A display map category, originally just called a class of display maps with a stability condition, can be used to model dependent type theory. [...] The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library."

https://resolver.tudelft.nl/uuid:25ddff49-8d20-40ce-bb35-3b3f986c65ff

#Master #Thesis #Rocq #HoTT #UnivalentFoundations #UniMath

Master thesis by José Padilla Cancio: "Integrating runtime identity functions into a dependent type system"

"We name functions between these types that behave like the identity at runtime, runtime identity (runid) functions. [..] This thesis introduces a lightweight core language that extends a QTT-style, intensional Martin-Löf Type Theory (MLTT) with explicit markers for runid functions."

https://resolver.tudelft.nl/uuid:e6d5e4a8-6df5-4867-ad9b-4ac77cdc2512

#thesis #TypeTheory #QTT #DependentTypes #agda

Master thesis by Julius de Jeu: "Detecting Undefined Behavior Across Foreign Function Boundaries in Rust Programs"

"[..] we propose a novel mechanism for detecting memory safety violations across language boundaries. We implemented it in a tool called MiriPBT: a combination of MIRI, a tool that can enforce ownership rules at runtime [..] and Property Based Testing, which allows us to greatly increase the size of the domain we can test."

https://resolver.tudelft.nl/uuid:dffbff9e-6bbc-491a-a00e-8754ce0fdd77

#master #thesis #Rust #MIRI

Master thesis by Arthur de Groot: Memoising Scope Graph Query Resolution

"In this thesis, we propose a memoised variant of the current state-of-the-art query resolution algorithm that memoises data encountered during graph traversal, reducing future queries to a cache lookup. [..] We construct a synthetic dataset with these patterns that is used to evaluate query resolution algorithms with microbenchmarks."

https://resolver.tudelft.nl/uuid:7c5ea32b-d4de-4c69-a5be-c866d6250547

#ScopeGraphs #Spoofax #Statix #LanguageEngineering #Thesis

Master thesis by Michał Raczkiewicz: "Model Checking Under JAM21"

"This thesis presents the first known implementation of a model checker for the Java memory model JAM21 within the GenMC framework - a tool for stateless model checking using custom memory models. [..] We provide a formal proof of equivalence between the new vector clock algorithm and the original implementation to ensure correctness."

https://repository.tudelft.nl/record/uuid:3c4c7d73-b084-4a4d-9d6d-93256bc09598

#Java #ModelChecking #MemoryModels #FormalProofs #master #thesis

Master thesis by Niyousha Najmaei: "The Internal Language of Comprehension Categories"

"[..] we propose a candidate type theory for the internal language of comprehension categories by extracting a type theory from the semantics given by a general comprehension category which is not full and split. We also give an interpretation of this type theory in every comprehension category."

https://repository.tudelft.nl/record/uuid:39e79d29-122c-4b54-827f-fd9908495e17

#TypeTheory #CategoryTheory #MLTT #thesis

"2-Functoriality of Initial Semantics, and Applications" by Benedikt Ahrens, Ambroise Lafont, and Thomas Lamiaux was accepted at #icfp

"We provide tools to compare and relate the models obtained from a signature for different choices of monoidal category [..] we use our results to relate the models of the different implementation [..] and to provide a generalized recursion principle for simply-typed syntax."

Read it on #arXiv: https://arxiv.org/abs/2503.10863

#TypeTheory #CategoryTheory

Master thesis by Hendy Liang: "Property-Based ASTs: Enabling Language Parametricity in Refactoring Tools"

"By leveraging Tree-Sitter, a parser generator that creates parsers that produce generic, property-based ASTs, this research adapts Renaissance, an existing industrial refactoring tool, to support multi-language extensibility with minimal additional effort."

https://repository.tudelft.nl/record/uuid:6e143a35-32b8-4f7e-928e-52057ea57566

#LanguageParametricity #refactoring #treesitter #thesis

Master thesis by Pepijn Vunderink: "Program Matching with Semantic Patterns"

"We propose the Dyno pattern language, in which concrete object language syntax can be used to express intuitive semantic patterns of programs. Pattern matching is performed by translating Dyno patterns to μ-calculus formulas and model checking these formulas against models extracted from object programs."

https://repository.tudelft.nl/record/uuid:a18ab135-96b1-417c-b25e-46aa02521896

#thesis #PatternMatching #MuCalculus #ModelChecking #mCRL2

Master thesis by Alexandru Dumitriu: "LLM-Driven Synthesis of Concurrent Data Structures with SMR under Weak Memory"

"This thesis introduces a synthesis-verification pipeline that iteratively generates concurrent data structures from partial code specifications [..] We evaluate our approach using established concurrent data structure benchmarks, demonstrating rapid convergence to correct implementations"

https://repository.tudelft.nl/record/uuid:5a857798-276f-4545-af2d-8a381e84df9a

#ProgramSynthesis #SMR #WeakMemory #master #thesis

Master thesis by Jochem Broekhoff: "Domain-Specific Abstractions for Algorithmic Graph Processing"

"The Green-Marl Intermediate Representation (GMIR) [..] prevents frontier exploration algorithms and community detection algorithms to be expressed, such as Dijkstra’s shortest path and the Louvain clustering method. We [..] introduce new domain-specific abstractions for algorithmic graph processing, targeting those algorithms."

https://repository.tudelft.nl/record/uuid:a4d57d94-811c-430f-8dd1-46d6a478feb1

#GreenMarl #GraphProcessing #dsl #thesis