Categories of containers, Proceedings of FOSSACS 2003, number 2620 in Lecture Notes in Computer Science, pp.23-38, 2003. ,
, , 2016.
Interactive programming in Agda-Objects and graphical user interfaces, Journal of Functional Programming, vol.27, 2017. ,
??: Dependent types without the sugar, Functional and Logic Programming, vol.6009, pp.40-55, 2010. ,
Coinductive data types, 2011. ,
The Agda Wiki, 2014. ,
, Talk given at the TYPES Workshop in Jouy-en-Josas, 2004.
Copatterns: Programming infinite structures by observations, Proceedings of POPL '13, pp.27-38, 2013. ,
Interactive Theorem Proving and Program Development, Texts in Theoretical Computer Science. An EATCS Series, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
CoInduction in Coq, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00001174
Type theory based on dependent inductive and coinductive types, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pp.327-336, 2016. ,
About charity, Yellow Series Report, 1992. ,
Infinite objects in type theory, Types for Proofs and Programs, vol.806, pp.62-78, 1994. ,
Subtyping, declaratively, Mathematics of Program Construction, vol.10, pp.100-118, 2010. ,
, , 2009.
A survey of recursive combinatorics, Handbook of Recursive Mathematics, vol.16, pp.80049-80058, 1998. ,
Inductive and coinductive types with iteration and recursion, formal proceedings of the 1992 workshop on Types for Proofs and Programs, pp.183-207, 1992. ,
Codifying guarded definitions with recursive schemes, Types for Proofs and Programs, vol.996, pp.39-59, 1995. ,
English: A calculus of infinite constructions and its application to the verification of communicating systems), 1996. ,
Reference and Computation in Intuitionistic Type Theory, 2008. ,
Programming with inductive and co-inductive types, vol.37, 1992. ,
A Categorical Programming Language, 1987. ,
, Codatatypes in ML. J. Symb. Comput, vol.8, issue.6, pp.80065-80068, 1989.
Inductive, coinductive, and pointed types, Proceedings of the first ACM SIGPLAN international conference on Functional programming, ICFP '96, pp.102-109, 1996. ,
Interactive programs in dependent type theory, CSL 2000, vol.1862, pp.317-331, 2000. ,
Interactive programs and weakly final coalgebras (extended version), Dependently typed programming, number 04381 in Dagstuhl Seminar Proceedings. Internationales Begegnungs-und Forschungszentrum (IBFI), 2004. ,
Interactive programs and weakly final coalgebras in dependent type theory, From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, pp.115-134, 2005. ,
The Coq Proof Assistant Reference Manual. INRIA, version 8 ,
Programming with monadic CSP-style processes in dependent type theory, Proceedings of the 1st International Workshop on Type-Driven Development, pp.28-38, 2016. ,
Trace and stable failures semantics for CSP-Agda, Proceedings of the First Workshop on Coalgebra, Horn Clause Logic Programming and Types, vol.258, pp.36-51, 2016. ,
Accepted for publication in Postproceedings TYPES, vol.23, 2016. ,
A tutorial on (co)algebras and (co)induction, EATCS Bulletin, vol.62, pp.62-222, 1997. ,
A symmetric form of Gödel's theorem, Ind. Math, vol.12, pp.244-246, 1950. ,
Let's see how things unfold: Reconciling the infinite with the intensional, Proceedings of the 3rd international Conference on Algebra and Coalgebra in Computer Science, CALCO'09, pp.113-126, 2009. ,
Recursive types and type constraints in second-order lambda calculus, Proceedings of the Second Annual IEEE Symp. on Logic in Computer Science, LICS 1987, pp.30-36, 1987. ,
Inductive types and type constraints in the second-order lambda calculus, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.159-172, 1991. ,
Towards a practical programming language based on dependent type theory, 2007. ,
Classical Recursion Theory, vol.125, pp.70011-70020, 1992. ,
Coinductive types and type preservation, 2008. ,
Extensions of some theorems of Gödel and Church, The Journal of Symbolic Logic, vol.1, issue.3, pp.87-91, 1936. ,
Universal coalgebra: a theory of systems, Theoretical Computer Science, vol.249, issue.1, pp.56-62, 2000. ,
Coalgebras as types determined by their elimination rules, of Logic, Epistemology, and the Unity of Science, vol.27, pp.351-369, 2012. ,
How to reason coinductively informally, Advances in Proof Theory, pp.377-408, 2016. ,
On recursive separability, Dokl. Acad. Nauk, vol.88, pp.953-956, 1953. ,
Elementary strong functional programming, Funtional Programming Languages in Education, vol.1022, pp.1-13, 1995. ,
Total functional programming, Journal of Universal Computer Science, vol.10, issue.7, pp.751-768, 2004. ,
Functional programming with apomorphisms (corecursion), Proceedings of the Estonian Academy of Sciences, vol.47, pp.147-161, 1998. ,