The following pages link to Thorsten Altenkirch (Q1652991):
Displaying 44 items.
- Quotient inductive-inductive types (Q1652995) (← links)
- Setoid type theory -- a syntactic translation (Q2176677) (← links)
- Constructing a universe for the setoid model (Q2233391) (← links)
- (Q2766796) (← links)
- (Q2778813) (← links)
- (Q2778814) (← links)
- A predicative analysis of structural recursion (Q2784165) (← links)
- Type theory in type theory using quotient inductive types (Q2828239) (← links)
- An Algebra of Pure Quantum Programming (Q2864167) (← links)
- From Reversible to Irreversible Computations (Q2870206) (← links)
- (Q2980980) (← links)
- Partiality, Revisited (Q2988390) (← links)
- A Categorical Semantics for Inductive-Inductive Definitions (Q3090862) (← links)
- Monads Need Not Be Endofunctors (Q3557858) (← links)
- ΠΣ: Dependent Types without the Sugar (Q3558328) (← links)
- (Q3560840) (← links)
- Subtyping, Declaratively (Q3575268) (← links)
- Higher-Order Containers (Q3576186) (← links)
- A UNIVERSE OF STRICTLY POSITIVE FAMILIES (Q3620616) (← links)
- Big-step normalisation (Q3638919) (← links)
- (Q4263807) (← links)
- (Q4281462) (← links)
- Towards a Cubical Type Theory without an Interval (Q4580224) (← links)
- (Q4649535) (← links)
- (Q4816996) (← links)
- When is a function a fold or an unfold? (Q4917036) (← links)
- (Q4945244) (← links)
- Categorical reconstruction of a reduction free normalization proof (Q5057474) (← links)
- Martin Hofmann’s contributions to type theory: Groupoids and univalence (Q5084306) (← links)
- Free Higher Groups in Homotopy Type Theory (Q5145336) (← links)
- The Integers as a Higher Inductive Type (Q5145619) (← links)
- A Partial Type Checking Algorithm for Type:Type (Q5166618) (← links)
- Monads need not be endofunctors (Q5177334) (← links)
- Relative Monads Formalised (Q5195253) (← links)
- (Q5278407) (← links)
- Small Induction Recursion (Q5300900) (← links)
- Generalizations of Hedberg’s Theorem (Q5300901) (← links)
- Functional and Logic Programming (Q5308026) (← links)
- Normalisation by Evaluation for Dependent Types. (Q5369471) (← links)
- (Q5371043) (← links)
- Indexed containers (Q5371943) (← links)
- Structuring quantum effects: superoperators as arrows (Q5482270) (← links)
- Types for Proofs and Programs (Q5897611) (← links)
- (Q6079230) (← links)
