Concept

Homotopy type theory

Related publications (17)

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

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

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

Decrypting Local Type Inference

Hubert Plociniczak

Statically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages ...

EPFL2016

A generic algorithm for checking exhaustivity of pattern matching

Fengyun Liu

Algebraic data types and pattern matching are key features of functional programming languages. Exhaustivity checking of pattern matching is a safety belt that defends against unmatched exceptions at runtime and boosts type safety. However, the presence of ...

2016

The homotopy theory of coalgebras over a comonad

Kathryn Hess Bellwald

Let K be a comonad on a model category M. We provide conditions under which the associated category of K-coalgebras admits a model category structure such that the forgetful functor to M creates both cofibrations and weak equivalences. We provide concrete ...

2014

Foundations of Path-Dependent Types

Martin Odersky, Tiark Rompf, 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. An essential ingredient of this unification is the concept of objects wit ...

Assoc Computing Machinery2014

Flow-induced uprooting of young vegetation on river bedforms

Paolo Perona, Benoît Crouzy, Katharina Maria Edmaier

Riparian vegetation stabilizes sediment by its roots and henceforth impacts riparian morphodynamics. After germination or vegetative reproduction on river bars or islands, juvenile plants are exposed to a high risk of mortality due to uprooting by floods. ...

Crc Press-Taylor & Francis Group2014

Complete Completion using Types and Weights

Viktor Kuncak, Ruzica Piskac, Tihomir Gvero, Ivan Kuraj

Developing modern software typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes ...

ACM2013

Dependent Object Types

Martin Odersky, Nada Amin

We propose a new type-theoretic foundation of Scala and languages like it: the Dependent Object Types (DOT) calculus. DOT models Scala’s path-dependent types, abstract type members and its mixture of nominal and structural typing through the use of reﬁneme ...

2012

Normal and conormal maps in homotopy theory

Kathryn Hess Bellwald

Let M be a monoidal category endowed with a distinguished class of weak equivalences and with appropriately compatible classifying bundles for monoids and comonoids. We define and study homotopy-invariant notions of normality for maps of monoids and of con ...

Int Press Boston, Inc2012

Homotopy theory of modules over operads in symmetric spectra

We establish model category structures on algebras and modules over operads in symmetric spectra and study when a morphism of operads induces a Quillen equivalence between corresponding categories of algebras (resp. modules) over operads. ...

2009

Coalgèbres d'Alexander-Whitney : un modèle algébrique pour les espaces topologiques

Théophile Naïto

The goal of this work is to study Alexander-Whitney coalgebras (first defined in [HPST06]) from a topological point of view. An Alexander-Whitney coalgebra is a coassociative chain coalgebra over Z with an extra algebraic structure : the comultiplication m ...

EPFL2009

A Core Calculus for Scala Type Checking

Martin Odersky, Vincent Cremet

We present a minimal core calculus that captures interesting constructs of the Scala programming language: nested classes, abstract types, mixin composition, and path dependent types. We show that the problems of type assignment and subtyping in this calcu ...

2006