Thierry Coquand

Proceedings of the Logics and Type Systems in Theory and Practice, 2024

Some Remarks About Dependent Type Theory.

[BibT_eX]

[DOI]

Proceedings of the French School of Programming, 2024

2023

Reduction Free Normalisation for a proof irrelevant type of propositions.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2023

2022

Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2022

Canonicity and homotopy canonicity for cubical type theory.

[BibT_eX]

[DOI]

Christian Sattler

Log. Methods Comput. Sci., 2022

Type Theories with Universe Level Judgements.

[BibT_eX]

[DOI]

CoRR, 2022

Controlling unfolding in type theory.

[BibT_eX]

[DOI]

CoRR, 2022

Type Theory with Explicit Universe Polymorphism.

[BibT_eX]

[DOI]

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

2021

Constructive sheaf models of type theory.

[BibT_eX]

[DOI]

Fabian Ruch

Christian Sattler

Math. Struct. Comput. Sci., 2021

On generalized algebraic theories and categories with families.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2021

Syntax and models of Cartesian cubical type theory.

[BibT_eX]

[DOI]

Kuen-Bang Hou (Favonia)

Daniel R. Licata

Math. Struct. Comput. Sci., 2021

Geometric Logic, Constructivisation, and Automated Theorem Proving (Dagstuhl Seminar 21472).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2021

2020

Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2020

A Note on Generalized Algebraic Theories and Categories with Families.

[BibT_eX]

[DOI]

CoRR, 2020

2019

Canonicity and normalization for dependent type theory.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2019

An Adequacy Theorem for Dependent Type Theory.

[BibT_eX]

[DOI]

Theory Comput. Syst., 2019

Preface to the special issue for The Fifth Workshop on Formal Topology.

[BibT_eX]

[DOI]

Maria Emilia Maietti

J. Log. Anal., 2019

The Univalence Axiom in Cubical Sets.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Skolem's Theorem in Coherent Logic.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2019

Homotopy Canonicity for Cubical Type Theory.

[BibT_eX]

[DOI]

Christian Sattler

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018

A survey of constructive presheaf models of univalence.

[BibT_eX]

[DOI]

ACM SIGLOG News, 2018

Canonicity and normalisation for Dependent Type Theory.

[BibT_eX]

[DOI]

CoRR, 2018

On Higher Inductive Types in Cubical Type Theory.

[BibT_eX]

[DOI]

Anders Mörtberg

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Inner Models of Univalence.

[BibT_eX]

[DOI]

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

The Independence of Markov's Principle in Type Theory.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.

[BibT_eX]

[DOI]

FLAP, 2017

Notions of Anonymous Existence in Martin-Löf Type Theory.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

Stack semantics of type theory.

[BibT_eX]

[DOI]

Fabian Ruch

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Type Theory and Formalisation of Mathematics.

[BibT_eX]

[DOI]

Proceedings of the Computer Science - Theory and Applications, 2017

2016

A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic.

[BibT_eX]

[DOI]

Robin Adams

CoRR, 2016

Preface.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2016

Realizability at Work: Separating Two Constructive Notions of Finiteness.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic.

[BibT_eX]

[DOI]

Robin Adams

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

The Ackermann Award 2016.

[BibT_eX]

[DOI]

Anuj Dawar

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

A Kripke model for simplicial sets.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2015

A generalization of the Takeuti-Gandy interpretation.

[BibT_eX]

[DOI]

Bruno Barras

Math. Struct. Comput. Sci., 2015

A Presheaf Model of Parametric Type Theory.

[BibT_eX]

[DOI]

Jean-Philippe Bernardy

Guilhem Moulin

Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics, 2015

Non-Constructivity in Kan Simplicial Sets.

[BibT_eX]

[DOI]

Erik Parmann

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

2014

A Sheaf Model of the Algebraic Closure.

[BibT_eX]

[DOI]

Proceedings of the Proceedings Fifth International Workshop on Classical Logic and Computation, 2014

2013

Computing persistent homology within Coq/SSReflect.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2013

Dynamic Newton-Puiseux theorem.

[BibT_eX]

[DOI]

J. Log. Anal., 2013

About Goodman's Theorem.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2013

A Model of Type Theory in Cubical Sets.

[BibT_eX]

[DOI]

Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

Generalizations of Hedberg's Theorem.

[BibT_eX]

[DOI]

Nicolai Kraus

Martín Hötzel Escardó

Thorsten Altenkirch

Proceedings of the Typed Lambda Calculi and Applications, 11th International Conference, 2013

2012

A Computational Interpretation of Forcing in Type Theory.

[BibT_eX]

[DOI]

Guilhem Jaber

Proceedings of the Epistemology versus Ontology, 2012

A constructive proof of Simpson's Rule.

[BibT_eX]

[DOI]

J. Log. Anal., 2012

A formal proof of Sasaki-Murao algorithm.

[BibT_eX]

[DOI]

Anders Mörtberg

Vincent Siles

J. Formaliz. Reason., 2012

Preface.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2012

Stop When You Are Almost-Full - Adventures in Constructive Termination.

[BibT_eX]

[DOI]

Dimitrios Vytiniotis

David Wahlstedt

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

The Ackermann Award 2012.

[BibT_eX]

[DOI]

Anuj Dawar

Damian Niwinski

Proceedings of the Computer Science Logic (CSL'12), 2012

Coherent and Strongly Discrete Rings in Type Theory.

[BibT_eX]

[DOI]

Anders Mörtberg

Vincent Siles

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Metric complements of overt closed sets.

[BibT_eX]

[DOI]

Math. Log. Q., 2011

Unique paths as formal points.

[BibT_eX]

[DOI]

Peter Schuster

J. Log. Anal., 2011

A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance

[BibT_eX]

[DOI]

Miguel Pagano

Log. Methods Comput. Sci., 2011

A Decision Procedure for Regular Expression Equivalence in Type Theory.

[BibT_eX]

[DOI]

Vincent Siles

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Curves and coherent Prüfer rings.

[BibT_eX]

[DOI]

Claude Quitté

J. Symb. Comput., 2010

Constructive theory of Banach algebras.

[BibT_eX]

[DOI]

J. Log. Anal., 2010

A Note on Forcing and Type Theory.

[BibT_eX]

[DOI]

Guilhem Jaber

Fundam. Informaticae, 2010

Games with 1-backtracking.

[BibT_eX]

[DOI]

Stefano Berardi

Susumu Hayashi

Ann. Pure Appl. Log., 2010

2009

Integrals and valuations.

[BibT_eX]

[DOI]

J. Log. Anal., 2009

Space of valuations.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2009

Spectral schemes as ringed lattices.

[BibT_eX]

[DOI]

Peter Schuster

Ann. Math. Artif. Intell., 2009

Forcing and Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 23rd international Workshop, 2009

2008

A note on the axiomatisation of real numbers.

[BibT_eX]

[DOI]

Math. Log. Q., 2008

Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 9th International Symposium, 2008

Constructive Mathematics and Functional Programming (Abstract).

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2008

2007

A proof of strong normalisation using domain theory.

[BibT_eX]

[DOI]

Arnaud Spiwack

Log. Methods Comput. Sci., 2007

The Completeness of Typing for Context-Semantics.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2007

Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2007

Towards Constructive Homological Algebra in Type Theory.

[BibT_eX]

[DOI]

Arnaud Spiwack

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements.

[BibT_eX]

[DOI]

Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 2007

2006

A logical approach to abstract algebra.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2006

Remarks on the equational theory of non-normalizing pure type systems.

[BibT_eX]

[DOI]

Gilles Barthe

J. Funct. Program., 2006

Preface.

[BibT_eX]

[DOI]

Bernhard Banaschewski

Giovanni Sambin

Ann. Pure Appl. Log., 2006

Alfa/Agda.

[BibT_eX]

[DOI]

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005

A Short Proof for the Krull Dimension of a Polynomial Ring.

[BibT_eX]

[DOI]

Am. Math. Mon., 2005

A constructive proof of the Peter-Weyl theorem.

[BibT_eX]

[DOI]

Math. Log. Q., 2005

Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems.

[BibT_eX]

[DOI]

J. Univers. Comput. Sci., 2005

A Logical Framework with Dependently Typed Records.

[BibT_eX]

[DOI]

Randy Pollack

Makoto Takeyama

Fundam. Informaticae, 2005

Completeness Theorems and lambda-Calculus.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

Automating Coherent Logic.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2005

Connecting a Logical Framework to a First-Order Logic Prover.

[BibT_eX]

[DOI]

Ulf Norell

Proceedings of the Frontiers of Combining Systems, 5th International Workshop, 2005

A Nilregular Element Property.

[BibT_eX]

[DOI]

Peter Schuster

Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

05021 Abstracts Collection -- Mathematics, Algorithms, Proofs.

[BibT_eX]

[DOI]

Marie-Françoise Roy

Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

05021 Executive Summary -- Mathematics, Algorithms, Proofs.

[BibT_eX]

[DOI]

Proceedings of the Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005

A Logical Approach to Abstract Algebra.

[BibT_eX]

[DOI]

Proceedings of the New Computational Paradigms, 2005

An elementary characterisation of Krull dimension.

[BibT_eX]

Marie-Françoise Roy

Proceedings of the From sets and types to topology and analysis, 2005

2004

Proof-theoretical analysis of order relations.

[BibT_eX]

[DOI]

Sara Negri

Jan von Plato

Arch. Math. Log., 2004

Formalising Bitonic Sort in Type Theory.

[BibT_eX]

[DOI]

Ana Bove

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

2003

A representation of stably compact spaces, and patch topology.

[BibT_eX]

[DOI]

Guo-Qiang Zhang

Theor. Comput. Sci., 2003

A syntactical proof of the Marriage Lemma.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2003

Newman's lemma - a case study in proof automation and geometric logic, Logic in Computer Science Column.

[BibT_eX]

Bull. EATCS, 2003

Inductively generated formal topologies.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 2003

Dynamical Method in Algebra: A Survey.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2003

2002

Metric Boolean algebras and constructive measure theory.

[BibT_eX]

[DOI]

Arch. Math. Log., 2002

2001

A Finitary Subsystem of the Polymorphic lambda-Calculus.

[BibT_eX]

[DOI]

Thorsten Altenkirch

Proceedings of the Typed Lambda Calculi and Applications, 5th International Conference, 2001

2000

Formal Topologies on The Set of First-Order Formulae.

[BibT_eX]

[DOI]

J. Symb. Log., 2000

Intuitionistic choice and classical logic.

[BibT_eX]

[DOI]

Arch. Math. Log., 2000

An Implementation of Type: Type.

[BibT_eX]

[DOI]

Makoto Takeyama

Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Sequents, Frames, and Completeness.

[BibT_eX]

[DOI]

Guo-Qiang Zhang

Proceedings of the Computer Science Logic, 2000

An Introduction to Dependent Type Theory.

[BibT_eX]

[DOI]

Gilles Barthe

Proceedings of the Applied Semantics, International Summer School, 2000

1999

A new method for establishing conservativity of classical systems over their intuitionistic version.

[BibT_eX]

[DOI]

Martin Hofmann

Math. Struct. Comput. Sci., 1999

A Boolean Model of Ultrafilters.

[BibT_eX]

[DOI]

Ann. Pure Appl. Log., 1999

1998

On the Computational Content of the Axiom of Choice.

[BibT_eX]

[DOI]

Stefano Berardi

J. Symb. Log., 1998

A Note on Formal Iterated Function Systems.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Real Number Computation, 1998

Two applications of Boolean models.

[BibT_eX]

[DOI]

Arch. Math. Log., 1998

Gröbner Bases in Type Theory.

[BibT_eX]

[DOI]

Henrik Persson

Proceedings of the Types for Proofs and Programs, 1998

1997

Intuitionistic Model Constructions and Normalization Proofs.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1997

Minimal Invariant Spaces in Formal Topology.

[BibT_eX]

[DOI]

J. Symb. Log., 1997

A Proof-Theoretical Investigation of Zantema's Problem.

[BibT_eX]

[DOI]

Henrik Persson

Proceedings of the Computer Science Logic, 11th International Workshop, 1997

1996

An Algorithm for Type-Checking Dependent Types.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1996

1995

A Semantics of Evidence for Classical Arithmetic.

[BibT_eX]

[DOI]

J. Symb. Log., 1995

An Application of Constructive Completeness.

[BibT_eX]

[DOI]

Jan M. Smith

Proceedings of the Types for Proofs and Programs, 1995

A realization of the negative interpretation of the Axiom of Choice.

[BibT_eX]

[DOI]

Stefano Berardi

Proceedings of the Typed Lambda Calculi and Applications, 1995

Program Construction in Intuitionistic Type Theory (Abstract).

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 1995

1994

An Analysis of Ramsey's Theorem

[BibT_eX]

[DOI]

Inf. Comput., May, 1994

A - Translation and Looping Combinators in Pure Type Systems.

[BibT_eX]

[DOI]

Hugo Herbelin

J. Funct. Program., 1994

Type Theorie Programming.

[BibT_eX]

Bull. EATCS, 1994

Inductive Definitions and Type Theory: an Introduction (Preliminary Version).

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1994

1993

Another Proof of the Intuitionistic Ramsey Theorem.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1993

Infinite Objects in Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1993

1992

An Intuitionistic Proof of Tychonoff's Theorem.

[BibT_eX]

[DOI]

J. Symb. Log., 1992

The Paradox of Trees in Type Theory.

[BibT_eX]

[DOI]

BIT, 1992

1991

Inheritance as Implicit Coercion

[BibT_eX]

[DOI]

Inf. Comput., July, 1991

A Direct Proof of the Intuitionistic Ramsey Theorem.

[BibT_eX]

[DOI]

Proceedings of the Category Theory and Computer Science, 1991

Constructive Topology and Combinatorics.

[BibT_eX]

[DOI]

Proceedings of the Constructivity in Computer Science, 1991

1989

Domain Theoretic Models of Polymorphism

[BibT_eX]

[DOI]

Carl A. Gunter

Glynn Winskel

Inf. Comput., May, 1989

Categories of Embeddings.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1989

Inheritance and Explicit Coercion (Preliminary Report)

[BibT_eX]

[DOI]

Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

1988

Extensional Models for Polymorphism.

[BibT_eX]

[DOI]

Val Tannen

Theor. Comput. Sci., 1988

The Calculus of Constructions

[BibT_eX]

[DOI]

Inf. Comput., 1988

Inductively defined types.

[BibT_eX]

[DOI]

Christine Paulin

Proceedings of the COLOG-88, 1988

1987

DI-Domains as a Model of Polymorphism.

[BibT_eX]

[DOI]

Carl A. Gunter

Glynn Winskel

Proceedings of the Mathematical Foundations of Programming Language Semantics, 1987

An Equational Presentation of Higher Order Logic.

[BibT_eX]

[DOI]

Thomas Ehrhard

Proceedings of the Category Theory and Computer Science, 1987

1986

An Analysis of Girard's Paradox

[BibT_eX]

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

1985

A Selected Bibliography on Constructive Mathematics, Intuitionistic Type Theory and Higher Order Deduction.

[BibT_eX]

[DOI]

J. Symb. Comput., 1985

Concepts mathématiques et informatiques formalisés dans le calcul des constructions.

[BibT_eX]

Proceedings of the Logic Colloquium '85, Orsay, France, 1985

Sur l'Analogie entre les Propositions et les Types.

[BibT_eX]

[DOI]

Proceedings of the Combinators and Functional Programming Languages, 1985

Constructions: A Higher Order Proof System for Mechanizing Mathematics.

[BibT_eX]

[DOI]