Peter Dybjer

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

2007

Towards Formalizing Categorical Models of Type Theory in Type Theory.

[BibT_eX]

[DOI]

Alexandre Buisse

Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007

Normalization by Evaluation for Martin-Löf Type Theory with One Universe.

[BibT_eX]

[DOI]

Andreas Abel

Klaus Aehlig

Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, 2007

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

[BibT_eX]

[DOI]

Andreas Abel

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

2006

Indexed induction-recursion.

[BibT_eX]

[DOI]

Anton Setzer

J. Log. Algebraic Methods Program., 2006

2004

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming.

[BibT_eX]

[DOI]

Gilles Barthe

Peter Thiemann

J. Funct. Program., 2004

Verifying Haskell programs by combining testing, model checking and interactive theorem proving.

[BibT_eX]

[DOI]

Inf. Softw. Technol., 2004

Random Generators for Dependent Types.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing, 2004

2003

Universes for Generic Programs and Proofs in Dependent Type Theory.

[BibT_eX]

Marcin Benke

Patrik Jansson

Nord. J. Comput., 2003

Induction-recursion and initial algebras.

[BibT_eX]

[DOI]

Anton Setzer

Ann. Pure Appl. Log., 2003

Combining Testing and Proving in Dependent Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Verifying Haskell Programs by Combining Testing and Proving.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Conference on Quality Software (QSIC 2003), 2003

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

2000

A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory.

[BibT_eX]

[DOI]

J. Symb. Log., 2000

Normalization and Partial Evaluation.

[BibT_eX]

[DOI]

Andrzej Filinski

Proceedings of the Applied Semantics, International Summer School, 2000

1999

A Finite Axiomatization of Inductive-Recursive Definitions.

[BibT_eX]

[DOI]

Anton Setzer

Proceedings of the Typed Lambda Calculi and Applications, 4th International Conference, 1999

1998

Normalization and the Yoneda Embedding.

[BibT_eX]

[DOI]

Djordje Cubric

Philip J. Scott

Math. Struct. Comput. Sci., 1998

1997

Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1997

Intuitionistic Model Constructions and Normalization Proofs.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 1997

1996

A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem.

[BibT_eX]

[DOI]

Sten Agerholm

Ilya Beylin

Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

1995

Internal Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, 1995

Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids.

[BibT_eX]

[DOI]

Ilya Beylin

Proceedings of the Types for Proofs and Programs, 1995

1994

Inductive Families.

[BibT_eX]

[DOI]

Formal Aspects Comput., 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

1991

Inverse Image Analysis Generalises Strictness Analysis

[BibT_eX]

[DOI]

Inf. Comput., February, 1991

1990

Comparing Integrated and External Logics of Functional Programs.

[BibT_eX]

[DOI]

Sci. Comput. Program., 1990

1989

A Functional Programming Approach to the Specification and Verification of Concurrent Systems.

[BibT_eX]

[DOI]

Herbert P. Sander

Formal Aspects Comput., 1989

1987

Inverse Image Analysis.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 14th International Colloquium, 1987

1985

Using Domain Algebras to Prove the Correctness of a Compiler.

[BibT_eX]

[DOI]

Proceedings of the STACS 85, 1985

Program Verification in a Logical Theory of Constructions.

[BibT_eX]

[DOI]

Proceedings of the Functional Programming Languages and Computer Architecture, 1985

Category Theory and Programming Language Semantics: an Overview.

[BibT_eX]

[DOI]

Proceedings of the Category Theory and Computer Programming, 1985

1984

Some Results on the Deductive Structure of Join Dependencies.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1984

Domain Algebras.

[BibT_eX]

[DOI]

Proceedings of the Automata, 1984

1983

Towards a Unified Theory of Data Types: Some Categorical Aspects.

[BibT_eX]