Publications

Bernardy, Jean-Philippe; Moulin, Guilhem: A Computational Interpretation of Parametricity. Logic in Computer Science, pp. 1-10.

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

Coquand, Thierry; Palmgren, E.; Spitters, B.: Metric complements of overt closed sets. Mathematical Logic Quarterly, 57 (4) pp. 373-378.

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

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

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)].

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.

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.

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

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.

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.

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.

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. Types for Proofs and Programs, April 2002, LNCS 2646 pp. 39--58. ISBN/ISSN: 3-540-14031-X

Coquand, Thierry; Lombardi, Henri: Hidden constructions in abstract algebra: Krull dimension of distributive lattices and commutative rings.. Commutative ring theory and applications (Fez, 2001), pp. 477--499.

Dybjer, Peter; Qiao, Haiyan; Takeyama, Makoto: Combining testing and proving in dependent type theory. Theorem Proving in Higher Order Logics, Rome, September 2003. LNCS, 2758 pp. 188-203.

Dybjer, Peter; Setzer, Anton: Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124 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.

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. Applied Semantics, Advanced Lectures, LNCS, 2395 pp. 137-192 .

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,

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.

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

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.

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,

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

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.

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

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

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.

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.

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