HoTT and Dependent Types Lab

← Voltar ao laboratório

Publicações

Agosto de 2021
Tesla Zhang

A Simpler Encoding of Indexed Types

Oficina ICFP 21 sobre o Desenvolvimento Orientado por Tipos — 2021

Janeiro de 2020
Fedor Part and Iddo Tzameret

Resolution with Counting: Dag-Like Lower Bounds and Different Moduli

11º Congresso sobre Inovações na Ciência da Computação Teórica (ITCS) 2020

Setembro de 2018
Valery Isaev

Contextually indexed contextual categories

arXiv

June 2018
Valery Isaev

Indexed type theories

arXiv

Abril de 2018
Valery Isaev

Morita equivalences between algebraic dependent type theories [Preprint]

arXiv

2018
Valery Isaev

On fibrant objects in model categories

Theory and Applications of Categories, Vol. 33, No. 3, 2018, pp. 43–66.

Setembro de 2017
Valery Isaev

Model structures on categories of models of type theories

Mathematical Structures in Computer Science

Outubro de 2016
Valery Isaev

Model category of marked objects

arXiv

2016 de fevereiro
Valery Isaev

Algebraic Presentations of Dependent Type Theories

arXiv

2016
Sergey Sinchuk , Pavel Chuprikov, Konstantin Solomatov

Verified operational transformation for trees

Interactive Theorem Proving (ITP)