Thorsten Altenkirch

Math. Struct. Comput. Sci., 2021

Should Type Theory replace Set Theory as the Foundation of Mathematics.

[BibT_eX]

[DOI]

CoRR, 2021

Constructing a universe for the setoid model.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2021

2020

The Integers as a Higher Inductive Type.

[BibT_eX]

[DOI]

Luis Scoccola

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

2019

Constructing quotient inductive-inductive types.

[BibT_eX]

[DOI]

András Kovács

Proc. ACM Program. Lang., 2019

Preface.

[BibT_eX]

[DOI]

Aleksy Schubert

Fundam. Informaticae, 2019

Big Step Normalisation for Type Theory.

[BibT_eX]

[DOI]

Colin Geniet

Proceedings of the 25th International Conference on Types for Proofs and Programs, 2019

Setoid Type Theory - A Syntactic Translation.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

2018

Free Higher Groups in Homotopy Type Theory.

[BibT_eX]

[DOI]

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

Pure Functional Epidemics: An Agent-Based Approach.

[BibT_eX]

[DOI]

Jonathan Thaler

Fredrik Nordvall Forsberg

Peer-Olaf Siebers

Proceedings of the 30th Symposium on Implementation and Application of Functional Languages, 2018

Quotient Inductive-Inductive Types.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2018

2017

Normalisation by Evaluation for Type Theory, in Type Theory.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

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

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2017

Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2017

2016

Selected papers from Dependently Typed Programming 2010 - Overview.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2016

Quotient inductive-inductive types.

[BibT_eX]

[DOI]

Fredrik Nordvall Forsberg

Paolo Capriotti

Gabe Dijkstra

CoRR, 2016

Normalisation by Evaluation for Dependent Types.

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Type theory in type theory using quotient inductive types.

[BibT_eX]

[DOI]

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Extending Homotopy Type Theory with Strict Equality.

[BibT_eX]

[DOI]

Paolo Capriotti

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

2015

Indexed containers.

[BibT_eX]

[DOI]

J. Funct. Program., 2015

Monads need not be endofunctors.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2015

Towards a Cubical Type Theory without an Interval.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Types for Proofs and Programs, 2015

2014

Relative Monads Formalised.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2014

Some constructions on ω-groupoids.

[BibT_eX]

[DOI]

Nuo Li

Ondrej Rypacek

Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2014

2013

Generalizations of Hedberg's Theorem.

[BibT_eX]

[DOI]

Martín Hötzel Escardó

Thierry Coquand

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

Small Induction Recursion.

[BibT_eX]

[DOI]

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

2012

A Syntactical Approach to Weak omega-Groupoids.

[BibT_eX]

[DOI]

Ondrej Rypacek

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

2011

A Categorical Semantics for Inductive-Inductive Definitions.

[BibT_eX]

[DOI]

Fredrik Nordvall Forsberg

Anton Setzer

Proceedings of the Algebra and Coalgebra in Computer Science, 2011

2010

Preface.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2010

Subtyping, Declaratively.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 10th International Conference, 2010

Termination Checking in the Presence of Nested Inductive and Coinductive Types.

[BibT_eX]

[DOI]

Proceedings of the Partiality and Recursion in Interactive Theorem Provers, 2010

Hereditary Substitutions for Simple Types, Formalized.

[BibT_eX]

[DOI]

Chantal Keller

Proceedings of the 3rd ACM SIGPLAN Workshop on Mathematically Structured Functional Programming, 2010

PiSigma: Dependent Types without the Sugar.

[BibT_eX]

[DOI]

Andres Löh

Nicolas Oury

Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

Higher-Order Containers.

[BibT_eX]

[DOI]

Paul Blain Levy

Sam Staton

Proceedings of the Programs, Proofs, Processes, 6th Conference on Computability in Europe, 2010

2009

Big-step normalisation.

[BibT_eX]

[DOI]

J. Funct. Program., 2009

A Universe of Strictly Positive Families.

[BibT_eX]

[DOI]

Int. J. Found. Comput. Sci., 2009

Indexed Containers.

[BibT_eX]

[DOI]

Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

2008

A Partial Type Checking Algorithm for Type: Type.

[BibT_eX]

[DOI]

Andreas Abel

Proceedings of the Second Workshop on Mathematically Structured Functional Programming, 2008

Dependent Types for Distributed Arrays.

[BibT_eX]

Wouter Swierstra

Proceedings of the Nineth Symposium on Trends in Functional Programming, 2008

2007

Observational equality, now!

[BibT_eX]

[DOI]

Wouter Swierstra

Proceedings of the ACM Workshop Programming Languages meets Program Verification, 2007

Beauty in the beast.

[BibT_eX]

[DOI]

Wouter Swierstra

Proceedings of the ACM SIGPLAN Workshop on Haskell, 2007

Constructing Strictly Positive Families.

[BibT_eX]

[DOI]

Proceedings of the Theory of Computing 2007. Proceedings of the Thirteenth Computing: The Australasian Theory Symposium (CATS2007). January 30, 2007

2006

Structuring quantum effects: superoperators as arrows.

[BibT_eX]

[DOI]

Juliana Kaizer Vizzotto

Amr Sabry

Math. Struct. Comput. Sci., 2006

From Reversible to Irreversible Computations.

[BibT_eX]

[DOI]

Alexander S. Green

Proceedings of the 4th International Workshop on Quantum Programming Languages, 2006

Generic Programming with Dependent Types.

[BibT_eX]

[DOI]

Proceedings of the Datatype-Generic Programming - International Spring School, 2006

Tait in One Big Step.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Mathematically Structured Functional Programming, 2006

2005

Containers: Constructing strictly positive types.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2005

for Data: Differentiating Data Structures.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2005

An Algebra of Pure Quantum Programming.

[BibT_eX]

[DOI]

Jonathan Grattage

Juliana Kaizer Vizzotto

Amr Sabry

Proceedings of the 3rd International Workshop on Quantum Programming Languages, 2005

Epigram reloaded: a standalone typechecker for ETT.

[BibT_eX]

Proceedings of the Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, 2005

A Functional Quantum Programming Language.

[BibT_eX]

[DOI]

Jonathan Grattage

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

2004

Exploring the Regular Tree Types.

[BibT_eX]

[DOI]

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

Constructing Polymorphic Programs with Quotient Types.

[BibT_eX]

[DOI]

Proceedings of the Mathematics of Program Construction, 7th International Conference, 2004

Representing Nested Inductive Types Using W-Types.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming: 31st International Colloquium, 2004

Normalization by Evaluation for lambda<sup>-2</sup>.

[BibT_eX]

[DOI]

Proceedings of the Functional and Logic Programming, 7th International Symposium, 2004

04381 Abstracts Collection - Dependently Typed Programming.

[BibT_eX]

[DOI]

Martin Hofmann

John Hughes

Proceedings of the Dependently Typed Programming, 12.09. - 17.09.2004, 2004

2003

Derivatives of Containers.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 6th International Conference, 2003

Categories of Containers.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2003

2002

A predicative analysis of structural recursion.

[BibT_eX]

[DOI]

Andreas Abel

J. Funct. Program., 2002

Generic Programming within Dependently Typed Programming.

[BibT_eX]

Proceedings of the Generic Programming, 2002

2001

When is a function a fold or an unfold?

[BibT_eX]

[DOI]

Jeremy Gibbons

Graham Hutton

Proceedings of the Coalgebraic Methods in Computer Science, 2001

A Finitary Subsystem of the Polymorphic lambda-Calculus.

[BibT_eX]

[DOI]

Thierry Coquand

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

Representations of First Order Function Types as Terminal Coalgebras.

[BibT_eX]

[DOI]

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

Normalization by Evaluation for Typed Lambda Calculus with Coproducts.

[BibT_eX]

[DOI]

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

1999

A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive Types.

[BibT_eX]

[DOI]

Andreas Abel

Proceedings of the Types for Proofs and Programs, 1999

Extensional Equality in Intensional Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Monadic Presentations of Lambda Terms Using Generalized Inductive Types.

[BibT_eX]

[DOI]

Bernhard Reus

Proceedings of the Computer Science Logic, 13th International Workshop, 1999

1998

Logical Relations and Inductive/Coinductive Types.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 12th International Workshop, 1998

1996

Reduction-Free Normalisation for a Polymorphic System.

[BibT_eX]

Martin Hofmann

Thomas Streicher

Proceedings of the Fourth Israel Symposium on Theory of Computing and Systems, 1996

1995

Categorical Reconstruction of a Reduction Free Normalization Proof.

[BibT_eX]

[DOI]

Martin Hofmann

Thomas Streicher

Proceedings of the Category Theory and Computer Science, 6th International Conference, 1995

1993

Proving Strong Normalization of CC by Modifying Realizability Semantics.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1993

A Formalization of the Strong Normalization Proof for System F in LEGO.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications, 1993

Constructions, inductive types and strong normalization.

[BibT_eX]