The following pages link to Peter Dybjer (Q651314):
Displaying 47 items.
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation (Q651316) (← links)
- Inverse image analysis generalises strictness analysis (Q751835) (← links)
- Some results on the deductive structure of join dependencies (Q798011) (← links)
- A functional programming approach to the specification and verification of concurrent systems (Q909439) (← links)
- Comparing integrated and external logics of functional programs (Q913479) (← links)
- Inductive families (Q1336951) (← links)
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory (Q1392287) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Finitary higher inductive types in the groupoid model (Q2130587) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- Intuitionistic model constructions and normalization proofs (Q2785696) (← links)
- Towards formalizing categorical models of type theory in type theory (Q2871881) (← links)
- Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs (Q2892763) (← links)
- Game Semantics and Normalization by Evaluation (Q2948551) (← links)
- The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories (Q3007659) (← links)
- A Brief Overview of Agda – A Functional Language with Dependent Types (Q3183520) (← links)
- (Q3216122) (← links)
- (Q3341950) (← links)
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory (Q3521979) (← links)
- (Q3677148) (← links)
- (Q3685173) (← links)
- (Q3757369) (← links)
- (Q3761674) (← links)
- (Q4012883) (← links)
- Normalization and the Yoneda embedding (Q4236219) (← links)
- (Q4263867) (← links)
- (Q4436029) (← links)
- (Q4470492) (← links)
- A general formulation of simultaneous inductive-recursive definitions in type theory (Q4508246) (← links)
- (Q4596801) (← links)
- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids (Q4647569) (← links)
- Internal type theory (Q4647575) (← links)
- (Q4813224) (← links)
- (Q4825542) (← links)
- Categories with Families: Unityped, Simply Typed, and Dependently Typed (Q5014596) (← links)
- On generalized algebraic theories and categories with families (Q5084311) (← links)
- Dependent Types at Work (Q5191088) (← links)
- Program Testing and the Meaning Explanations of Intuitionistic Type Theory (Q5253930) (← links)
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe (Q5262927) (← links)
- (Q5277836) (← links)
- The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective (Q5415629) (← links)
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (Q5458424) (← links)
- Theoretical Aspects of Computing - ICTAC 2004 (Q5709985) (← links)
- The biequivalence of locally cartesian closed categories and Martin-Löf type theories (Q5740406) (← links)
- A comparison of HOL and ALF formalizations of a categorical coherence theorem (Q6567701) (← links)
- The extended predicative Mahlo universe in Martin-Löf type theory (Q6636674) (← links)
- Type theory with explicit universe polymorphism (Q6643043) (← links)
