Peter Dybjer

	2012
49		Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez: Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. FoSSaCS 2012: 104-118
48		Peter Dybjer, Denis Kuperberg: Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation. Ann. Pure Appl. Logic 163(2): 122-131 (2012)
	2011
47		Pierre Clairambault, Peter Dybjer: The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. TLCA 2011: 91-106
46		Pierre Clairambault, Peter Dybjer: The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories CoRR abs/1112.3456: (2011)
	2009
45		Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez: Embedding a logical theory of constructions in Agda. PLPV 2009: 59-66
44		Ana Bove, Peter Dybjer, Ulf Norell: A Brief Overview of Agda - A Functional Language with Dependent Types. TPHOLs 2009: 73-78
	2008
43		Andreas Abel, Thierry Coquand, Peter Dybjer: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008: 3-13
42		Ana Bove, Peter Dybjer: Dependent Types at Work. LerNet ALFA Summer School 2008: 57-99
41		Andreas Abel, Thierry Coquand, Peter Dybjer: Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. MPC 2008: 29-56
40		Alexandre Buisse, Peter Dybjer: Towards Formalizing Categorical Models of Type Theory in Type Theory. Electr. Notes Theor. Comput. Sci. 196: 137-151 (2008)
39		Alexandre Buisse, Peter Dybjer: The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. Electr. Notes Theor. Comput. Sci. 218: 21-32 (2008)
	2007
38		Andreas Abel, Thierry Coquand, Peter Dybjer: Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. LICS 2007: 3-12
37		Andreas Abel, Klaus Aehlig, Peter Dybjer: Normalization by Evaluation for Martin-Löf Type Theory with One Universe. Electr. Notes Theor. Comput. Sci. 173: 17-39 (2007)
	2006
36		Peter Dybjer, Anton Setzer: Indexed induction-recursion. J. Log. Algebr. Program. 66(1): 1-49 (2006)
	2004
35		Peter Dybjer, Qiao Haiyan, Makoto Takeyama: Random Generators for Dependent Types. ICTAC 2004: 341-355
34		Peter Dybjer, Qiao Haiyan, Makoto Takeyama: Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Information & Software Technology 46(15): 1011-1025 (2004)
33		Gilles Barthe, Peter Dybjer, Peter Thiemann: Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. J. Funct. Program. 14(1): 1-2 (2004)
	2003
32		Peter Dybjer, Qiao Haiyan, Makoto Takeyama: Verifying Haskell Programs by Combining Testing and Proving. QSIC 2003: 272-279
31		Peter Dybjer, Qiao Haiyan, Makoto Takeyama: Combining Testing and Proving in Dependent Type Theory. TPHOLs 2003: 188-203
30		Peter Dybjer, Anton Setzer: Induction-recursion and initial algebras. Ann. Pure Appl. Logic 124(1-3): 1-47 (2003)
29		Marcin Benke, Peter Dybjer, Patrik Jansson: Universes for Generic Programs and Proofs in Dependent Type Theory. Nord. J. Comput. 10(4): 265-289 (2003)
	2002
28		Gilles Barthe, Peter Dybjer, Luis Pinto, João Saraiva: Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures Springer 2002
	2001
27		Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott: Normalization by Evaluation for Typed Lambda Calculus with Coproducts. LICS 2001: 303-310
26		Peter Dybjer, Anton Setzer: Indexed Induction-Recursion. Proof Theory in Computer Science 2001: 93-113
	2000
25		Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan M. Smith: Types for Proofs and Programs, International Workshop TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers Springer 2000
24		Peter Dybjer, Andrzej Filinski: Normalization and Partial Evaluation. APPSEM 2000: 137-192
23		Peter Dybjer: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. J. Symb. Log. 65(2): 525-549 (2000)
	1999
22		Peter Dybjer, Anton Setzer: A Finite Axiomatization of Inductive-Recursive Definitions. TLCA 1999: 129-146
	1998
21		Djordje Cubric, Peter Dybjer, Philip J. Scott: Normalization and the Yoneda Embedding. Mathematical Structures in Computer Science 8(2): 153-192 (1998)
	1997
20		Thierry Coquand, Peter Dybjer: Intuitionistic Model Constructions and Normalization Proofs. Mathematical Structures in Computer Science 7(1): 75-94 (1997)
19		Peter Dybjer: Representing Inductively Defined Sets by Wellorderings in Martin-Löf's Type Theory. Theor. Comput. Sci. 176(1-2): 329-335 (1997)
	1996
18		Sten Agerholm, Ilya Beylin, Peter Dybjer: A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. TPHOLs 1996: 17-32
	1995
17		Peter Dybjer, Bengt Nordström, Jan M. Smith: Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers Springer 1995
16		Peter Dybjer: Internal Type Theory. TYPES 1995: 120-134
15		Ilya Beylin, Peter Dybjer: Extracting a Proof of Coherence for Monoidal Categories from a Proof of Normalization for Monoids. TYPES 1995: 47-61
	1994
14		Thierry Coquand, Peter Dybjer: Inductive Definitions and Type Theory: an Introduction (Preliminary Version). FSTTCS 1994: 60-76
13		Peter Dybjer: Inductive Families. Formal Asp. Comput. 6(4): 440-465 (1994)
	1991
12		Peter Dybjer: Inverse Image Analysis Generalises Strictness Analysis Inf. Comput. 90(2): 194-216 (1991)
	1990
11		Peter Dybjer: Comparing Integrated and External Logics of Functional Programs. Sci. Comput. Program. 14(1): 59-79 (1990)
	1989
10		David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, Axel Poigné: Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings Springer 1989
9		Peter Dybjer, Herbert P. Sander: A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Formal Asp. Comput. 1(4): 303-319 (1989)
	1988
8		Peter Dybjer, Herbert P. Sander: A Functional Programming Approach to the Specification and Verification of Concurrent Systems. Specification and Verification of Concurrent Systems 1988: 331-343
	1987
7		Peter Dybjer: Inverse Image Analysis. ICALP 1987: 21-30
	1985
6		Peter Dybjer: Category Theory and Programming Language Semantics: an Overview. CTCS 1985: 165-181
5		Peter Dybjer: Program Verification in a Logical Theory of Constructions. FPCA 1985: 334-349
4		Peter Dybjer: Using Domain Algebras to Prove the Correctness of a Compiler. STACS 1985: 98-108
	1984
3		Peter Dybjer: Domain Algebras. ICALP 1984: 138-150
2		Peter Dybjer: Some Results on the Deductive Structure of Join Dependencies. Theor. Comput. Sci. 33: 95-105 (1984)
	1983
1		Peter Dybjer: Towards a Unified Theory of Data Types: Some Categorical Aspects. ADT 1983

Coauthor Index

1	Andreas Abel	[37] [38] [41] [43]
2	Klaus Aehlig	[37]
3	Sten Agerholm	[18]
4	Thorsten Altenkirch	[27]
5	Gilles Barthe	[28] [33]
6	Marcin Benke	[29]
7	Ilya Beylin	[15] [18]
8	Ana Bove	[42] [44] [45] [49]
9	Alexandre Buisse	[39] [40]
10	Pierre Clairambault	[46] [47]
11	Thierry Coquand	[14] [20] [25] [38] [41] [43]
12	Djordje Cubric	[21]
13	Andrzej Filinski	[24]
14	Qiao Haiyan	[31] [32] [34] [35]
15	Martin Hofmann	[27]
16	Patrik Jansson	[29]
17	Denis Kuperberg	[48]
18	Bengt Nordström	[17] [25]
19	Ulf Norell	[44]
20	Luis Pinto	[28]
21	David H. Pitt	[10]
22	Andrew M. Pitts	[10]
23	Axel Poigné	[10]
24	David E. Rydeheard	[10]
25	Herbert P. Sander	[8] [9]
26	João Saraiva	[28]
27	Philip J. Scott	[21] [27]
28	Anton Setzer	[22] [26] [30] [36]
29	Andrés Sicard-Ramírez	[45] [49]
30	Jan M. Smith	[17] [25]
31	Makoto Takeyama	[31] [32] [34] [35]
32	Peter Thiemann	[33]

Colors in the list of coauthors

Last update Fri May 25 01:42:58 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page