Concept

Homotopy type theory

Related publications (33)

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Cochains are all you need

In this thesis, we apply cochain complexes as an algebraic model of space in a diverse range of mathematical and scientific settings. We begin with an algebraic-discrete Morse theory model of auto-encoding cochain data, connecting the homotopy theory of d ...

EPFL2024

Real-time Self-contact Retargeting of Avatars down to Finger Level

Ronan Boulic, Bruno Herbelin, Mathias Guy Delahaye

We interact with the world through a body that includes hands and fingers. Likewise, providing an avatar allowing the control of a virtual body with fingers is an important step to improve the user experience in VR. When the user and their avatar skeleton ...

Jean-Marie Normand and Maki Sugimoto and Veronica Sundstedt2023

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we m ...

EPFL2022

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

ASSOC COMPUTING MACHINERY2022

Homotopical relations between 2-dimensional categories and their infinity-analogues

Lyne Moser

In this thesis, we study the homotopical relations of 2-categories, double categories, and their infinity-analogues. For this, we construct homotopy theories for the objects of interest, and show that there are homotopically full embeddings of 2-categories ...

EPFL2021

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain, Jonathan Immanuel Brachthäuser

2021

Relative Homological Algebra Via Truncations

Jérôme Scherer

To do homological algebra with unbounded chain complexes one needs to first find a way of constructing resolutions. Spal-tenstein solved this problem for chain complexes of R-modules by truncating further and further to the left, resolving the pieces, and ...

FIZ KARLSRUHE-LEIBNIZ-INST INFORMATIONSINFRASTRUKTUR2018

The Essence of Dependent Object Types

Martin Odersky, Tiark Rompf, Nada Amin, Sandro Stucki, Karl Samuel Grütter

Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus D-

Springer International Publishing2016

Dependent Object Types

Nada Amin

A scalable programming language is one in which the same concepts can describe small as well as large parts. Towards this goal, Scala unifies concepts from object and module systems. In particular, objects can contain type members, which can be selected as ...

EPFL2016

Implementing Higher-Kinded Types in Dotty

Martin Odersky, Guillaume André Fradji Martres, Dmytro Petrashko

dotty is a new, experimental Scala compiler based on DOT, the calculus of Dependent Object Types. Higher-kinded types are a natural extension of first-order lambda calculus, and have been a core construct of Haskell and Scala. As long as such types are jus ...

ACM2016