Publications

2012

Bernardy, Jean-Philippe; Moulin, Guilhem: A Computational Interpretation of Parametricity. IEEE Symposium on Logic in Computer Science. 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Dubrovnik, Croatia, June 25-28, 2012, pp. 135-144. ISBN/ISSN: 978-0-7695-4769-5

Bernardy, Jean-Philippe; Moulin, Guilhem: Type-Theory in Color.

Bove, Ana; Dybjer, Peter; Andrés, Sicard-Ramírez: Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. Lecture Notes in Computer Science. 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, 24 March - 1 April 2012, 7213 pp. 104-118. ISBN/ISSN: 978-3-642-28728-2

2011

Bernardy, Jean-Philippe; Moulin, Guilhem: Towards a computational interpretation of parametricity.

Danielsson, Nils Anders; Norell, Ulf: Parsing mixfix operators . Lecture Notes in Computer Science, 20th International Symposium on Implementation and Application of Functional Languages, IFL 2008, Hatfield, 10 September through 12 September 2008, 5836 pp. 80-99. ISBN/ISSN: 978-364224451-3

2010

Bove, Ana; Komendantskaya, Ekaterina; Niqui, Milad: Proceedings of the workshop on Partiality and Recursion in Interactive Theorem Provers. ISBN/ISSN: 2075-2180

2009

Bove, Ana; Dybjer, Peter; Norell, Ulf: A Brief Overview of Agda - A Functional Language with Dependent Types. Theorem Proving in Higher Order Logics , 5674 (LNCS) pp. 73--78.

Bove, Ana: Another Look at Function Domains. Mathematical Foundations of Programming Semantics, 25th Annual Conference, 249 (ENTCS) pp. 61-74.

Bove, Ana; Dybjer, Peter: Dependent Types at Work. Language Engineering and Rigorous Software Development, International LerNet ALFA Summer Schoo, 5520 (LNCS) pp. 57--99.

Bove, Ana; Dybjer, Peter; Sicard-Ramirez, Andres: Embedding a Logical Theory of Constructions in Agda. Programming Languages meets Program Verification (PLPV) 2009 , (ACM digital library)

Language Engineering and Rigorous Software Development. Ana Bove, Luis Barbosa, Alberto Pardo, Jorge Sousa Pinto [editor(s)].

2008

Abel, Andreas; Coquand, Thierry; Dybjer, Peter: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008, pp. 3-13.

Abel, Andreas; Coquand, Thierry; Dybjer, Peter: Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory. Mathematics of Program Construction 2008, pp. 29-56.

Bove, Ana; Capretta, Venanzio: A Type of Partial Recursive Functions. Theorem Proving in Higher Order Logics, 21st International Conference TPHOLs 2008, LNCS 5170 pp. 102--117. ISBN/ISSN: 978-3-540-71065-3

Danielsson, Nils Anders: Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. Conference record of the 35th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2008),

Dybjer, Peter; Buisse, Alexandre: The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories - an Intuitionistic Perspective. Electr. Notes Theor. Comput. Sci., (218) pp. 21-32.

2007

Abel, Andreas; Coquand, Thierry; Dybjer, Peter: Normalization by Evaluation for Martin-Löf Type Theory with Equality Judgements. Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007.,

Abel, Andreas; Aehlig, Klaus; Dybjer, Peter: Normalization by evaluation for Martin-Löf type theory with one universe. Mathematical Foundations of Programming Semantics, New Orleans, LA, USA, April 2007. Ed. M. Fiore. Electronic Notes in Theoretical Computer Science, Elsevier., 173 pp. 17-40.

Abel, Andreas; Coquand, Thierry: Untyped algorithmic equality for with surjective pairs Martin-Lof's logical framework. Fundamenta Informaticae, 77 (4) pp. 345-395.

Bove, Ana; Capretta, Venanzio: Computation by Prophecy. Typed Lambda Calculus and Applications; Simona Ronchi Della Rocca (Ed.), 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings. (Lecture notes in computer science; 4583 ), pp. 70--83. ISBN/ISSN: 978-3-540-73227-3

Buisse, Alexandre; Dybjer, Peter: Towards formalizing categorical models of type theory in type theory. Second International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP'07), eds Brigite Pientka and Carsten Schurmann, Electronic Notes in Theoretical Computer Science, Elsevier , pp. 72-85.

Danielsson, Nils Anders: A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family. Thorsten Altenkirch and Conor McBride (Eds.): Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 2006, Revised Selected Papers, LNCS 4502 pp. 93-109. ISBN/ISSN: 978-3-540-74463-4

Danielsson, Nils Anders: A Formalisation of the Correctness Result From "Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures".

Danielsson, Nils Anders: Functional Program Correctness Through Types. Göteborg : Chalmers University of Technology. Diss. ISBN/ISSN: 978-91-7385-034-6

Danielsson, Nils Anders: Proofs Accompanying "Fast and Loose Reasoning is Morally Correct".

Jansson, Patrik; Jeuring, Johan: Testing Properties of Generic Functions. LNCS, Proceedings of IFL 2006, 4449

Norell, Ulf: Towards a practical programming language based on dependent type theory. Göteborg : Chalmers University of Technology. Diss. ISBN/ISSN: 978-91-7291-996-9

2006

Coquand, Thierry: Geometric Hahn-Banach theorem. Math. Proc. Cambridge Philos. Soc, 140 (2) pp. 313-315.

Danielsson, Nils Anders; Hughes, John; Jansson, Patrik; Gibbons, Jeremy: Fast and Loose Reasoning is Morally Correct. Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 2006), pp. 206-217. ISBN/ISSN: 1-59593-027-2

Dybjer, Peter; Setzer, Anton: Indexed induction-recursion. Journal of Logic and Algebraic Programming, 66 (1) pp. 1-49.

Jansson, Patrik; Jeuring, Johan: Testing Properties of Generic Functions.

2005

Abel, Andreas; Matthes, R.; Uustalu, T.: Iteration and coiteration schemes for higher-order and nested datatypes. Theoretical Computer Science, 333 (1-2) pp. 3-66.

Abel, Andreas; Benke, Marcin; Bove, Ana; Hughes, John; Norell, Ulf: Verifying Haskell Programs Using Constructive Type Theory. Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell, ISBN/ISSN: 1-59593-071-X

Bove, Ana; Coquand, Thierry: Formalising Bitonic Sort in Type Theory. Types for Proofs and Programs TYPES 2004, LNCS 3839 pp. 82-97.

Bove, Ana; Capretta, Venanzio: Modelling General Recursion in Type Theory. Mathematical Structures in Computer Science, 15 pp. 671--708.

Bove, Ana; Capretta, Venanzio: Recursive Functions with Higher Order Domains. Typed Lambda Calculus and Applications TLCA 2005, (LNCS 3461) pp. 116--130.

Coquand, Thierry; Lombardi, Henri; Schuster, Peter: A nilregular element property.. Arch. Math. (Basel), 85 pp. 49-54.

Coquand, Thierry; Abel, Andreas: Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs. . Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005); in: LECTURE NOTES IN COMPUTER SCIENCE , Volume: 3461) , pp. 23-38.

2004

Bove, Ana: Formalising Bitonic Sort using Dependent Types. Göteborg : Chalmers University of Technology.

Danielsson, Nils Anders; Jansson, Patrik: Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values. Proceedings of the 7th International Conference on Mathematics of Program Construction, MPC 2004, LNCS 3125, pp. 85-109. ISBN/ISSN: 3-540-22380-0

Dybjer, Peter; Qiao, Haiyan; Takeyama, Makoto: Random generators for dependent types. Proceedings of the First International Colloquium on Theoretical Aspects of Computing, Guiyang, China, September 2004, pp. 342 -356 .

Dybjer, Peter; Haiyan, Qiao; Takeyama, Makoto: Verifying Haskell programs by combining testing, model checking and interactive theorem proving. Information and Software Technology, special issue, edited by Huimin Lin, Hans-Dieter Ehrich, and T.H. Tse, 46 (15) pp. 1011 - 1025.

Norell, Ulf; Jansson, Patrik: Polytypic Programming in Haskell. Implementation of Functional Languages, LNCS (3145) pp. 168-184.

Norell, Ulf; Jansson, Patrik: Prototyping Generic Programming in Template Haskell. Mathematics of Program Construction, LNCS (3125) pp. 314-333. ISBN/ISSN: 3-540-22380-0

Wahlstedt, David: Type Theory with First-Order Data Types and Size-Change Termination. Göteborg : Chalmers University of Technology.

2003

Benke, Marcin; Dybjer, Peter; Jansson, Patrik: Universes for Generic Programs and Proofs in Dependent Type Theory. Nordic Journal of Computing, 10 (4) pp. 265-289.

Bove, Ana: General Recursion in Type Theory. Lecture Notes in Computer Science. International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24–28, 2002, 2646 pp. 39-58. ISBN/ISSN: 978-3-540-14031-3

Coquand, Thierry; Lombardi, Henri: Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings. Commutative ring theory and applications. 4th International Conference on Commutative Algebra, Fez, 2001, 231 pp. 477-499. ISBN/ISSN: 0-8247-0855-5

Dybjer, Peter; Qiao, Haiyan; Takeyama, Makoto: Combining testing and proving in dependent type theory. Lecture Notes in Computer Science. Proceedings - 16th International Conference on Theorem Proving in Higher Order Logics, Rome, 8-12 September 2003, 2758 pp. 188-203. ISBN/ISSN: 3-540-40664-6

Dybjer, Peter; Setzer, Anton: Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124 (1-3) pp. 1-47.

Dybjer, Peter; Qiao, Haiyan; Takeyama, Makoto: Verifying Haskell programs by combining testing and proving. Proceedings 3rd International Conference on Quality Software, IEEE Computer Society Press, pp. 272-279. ISBN/ISSN: 0-7695-2015-4

2002

Bove, Ana: General Recursion in Type Theory. Göteborg : Chalmers University of Technology. Diss.

Bove, Ana: Generalised Simultaneous Inductive-Recursive Definitions and their Application to Programming in Type Theory. Göteborg : Chalmers University of Technology.

Bove, Ana: Mutual General Recursion in Type Theory. Göteborg : Chalmers University of Technology.

Dybjer, Peter; Filinski, Andrzej: Normalization and Partial Evaluation. Lecture Notes in Computer Science. International Summer School, APPSEM 2000 Caminha, Portugal, September 9–15, 2000, 2395 pp. 137-192 . ISBN/ISSN: 978-3-540-44044-4

Jansson, Patrik; Jeuring, Johan: Polytypic Data Conversion Programs. Science of Computer Programming, 43 (1) pp. 35-75.

Nordström, Bengt: Constructivism. A Computing Science Perspective.. Invited talk to the meeting on Foundations and the Ontological Quest in Pontificial Lateran University, Vatican City, January 2002,

2001

Dybjer, Peter; Setzer, Anton: Indexed induction-recursion. Proof Theory in Computer Science · International Seminar, LNCS, 2183 pp. 93-113.

Dybjer, Peter; Altenkirch, Thorsten; Hofmann, Martin; Scott, Philip: Normalization by evaluation for typed lambda calculus with coproducts. Proceedings of 16th Annual Symposium on Logic in Computer Science, pp. 203-210.

2000

Dybjer, Peter: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65 (2) pp. 525-549.

Jansson, Patrik; Jeuring, Johan: A Framework for Polytypic Programming on Terms, with an Application to Rewriting. Workshop on Generic Programming,

Nordström, Bengt; Petersson, Kent; Smith, Jan: Martin-Löf's Type Theory. Handbook of Logic in Computer Science, 5

1999

Backhouse, Roland; Jansson, Patrik; Jeuring, Johan; Meertens, Lambert: Generic Programming: An Introduction. Advanced Functional Programming, 1608 pp. 28--115.

Dybjer, Peter; Setzer, Anton: A finite axiomatization of inductive-recursive definitions. Proceedings of TLCA 1999, LNCS, 1581 pp. 129 - 146.

Jansson, Patrik; Jeuring, Johan: Polytypic Compact Printing and Parsing. European Symposium on Programming, 1576 pp. 273-287.

1998

Dybjer, Peter; Cubric, Djordje; Scott, Philip: Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8 pp. 153-192.

Jansson, Patrik; Jeuring, Johan: Functional Pearl: Polytypic Unification. Journal of Functional Programming, 8 (5) pp. 527-536.

Jansson, Patrik; Jeuring, Johan: PolyLib - a polytypic function library. Workshop on Generic Programming,

1997

Dybjer, Peter; Coquand, Thierry: Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7 pp. 75-94.

Dybjer, Peter: Representing inductively defined sets by well-orderings in Martin-Löf's type theory. Theoretical Computer Science, 176 pp. 329-335.

Jansson, Patrik: Functional Polytypic Programming --- Use and Implementation. Göteborg : Chalmers University of Technology. ISBN/ISSN: 91-7197 486-5

Jansson, Patrik; Jeuring, Johan: PolyP - a polytypic programming language extension. Principles of Programming Languages, POPL97 pp. 470-482. ISBN/ISSN: 0-89791-853-3

1996

Dybjer, Peter; Beylin, Ilya; Agerholm, Sten: A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. Theorem Proving in Higher Order Logics, LNCS, 1125 pp. 17-32.

Dybjer, Peter; Beylin, Ilya: Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids. TYPES '95, LNCS, 1158 pp. 47-61.

Dybjer, Peter: Internal type theory. TYPES '95, LNCS, 1158 pp. 120-134.

Jeuring, Johan; Jansson, Patrik: Polytypic Programming. Advanced Functional Programming, pp. 68-114.

1994

Dybjer, Peter: Inductive Families. Formal Aspects of Computing, 6 pp. 440-465.

Dybjer, Peter; Coquand, Thierry: Inductive definitions and type theory an introduction. Foundation of Software Technology and Theoretical Computer Science: 14th Conference Madras, India, LNCS, 880

1993

Dybjer, Peter; Coquand, Thierry: Intuitionistic model constructions and normalization proofs. Proceedings of the 1993 TYPES Workshop, Nijmegen,

1991

Dybjer, Peter: Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics. Logical Frameworks, pp. 280-306.

Dybjer, Peter: Inverse image analysis generalises strictness analysis. Information and Computation, 90 (2) pp. 194--216.

1990

Dybjer, Peter: Comparing integrated and external logics of functional programs. Science of Computer Programming, 14 pp. 59--79.

Nordström, Bengt; Petersson, Kent; Smith, Jan: Programming in Martin-Löf's Type Theory. Göteborg : Chalmers University of Technology.

1989

Dybjer, Peter; Sander, Herbert: A functional programming approach to the specification and verification of concurrent systems. Formal Aspects of Computing, 1 pp. 303-319.