References

  1. Andreas Abel & Thorsten Altenkirch (2002): A Predicative Analysis of Structural Recursion. J. Func. Program. 12(1), pp. 1–41, doi:10.1017/S0956796801004191.
  2. Andreas Abel (2006): A Polymorphic Lambda-Calculus with Sized Higher-Order Types. Ph.D. thesis. Ludwig-Maximilians-Universität München.
  3. Andreas Abel (2007): Mixed Inductive/Coinductive Types and Strong Normalization. In: Zhong Shao: Proc. of the 5th Asian Symp. on Programming Languages and Systems, APLAS 2007, Lect. Notes in Comput. Sci. 4807. Springer, pp. 286–301, doi:10.1007/978-3-540-76637-7_19.
  4. Andreas Abel (2008): Polarized Subtyping for Sized Types. Math. Struct. in Comput. Sci. 18, pp. 797–822, doi:10.1017/S0960129508006853. Special issue on subtyping, edited by Healfdene Goguen and Adriana Compagnoni..
  5. Andreas Abel (2008): Semi-continuous Sized Types and Termination. Logical Meth. in Comput. Sci. 4(2), doi:10.2168/LMCS-4(2:3)2008. CSL'06 special issue..
  6. Andreas Abel (2010): MiniAgda: Integrating Sized and Dependent Types. In: Ana Bove, Ekaterina Komendantskaya & Milad Niqui: Wksh. on Partiality And Recursion in Interactive Theorem Provers (PAR 2010), Electr. Proc. in Theor. Comp. Sci. 43, pp. 14–28, doi:10.4204/EPTCS.43.2.
  7. Andreas Abel (2011): Irrelevance in Type Theory with a Heterogeneous Equality Judgement. In: Martin Hofmann: Proc. of the 14th Int. Conf. on Foundations of Software Science and Computational Structures, FOSSACS 2011, Lect. Notes in Comput. Sci. 6604. Springer, pp. 57–71, doi:10.1007/978-3-642-19805-2_5.
  8. David Aspinall & Adriana B. Compagnoni (2001): Subtyping dependent types. Theor. Comput. Sci. 266(1-2), pp. 273–309, doi:10.1016/S0304-3975(00)00175-4.
  9. Roberto M. Amadio & Solange Coupet-Grimal (1998): Analysis of a Guard Condition in Type Theory (Extended Abstract).. In: Maurice Nivat: Proc. of the 1st Int. Conf. on Foundations of Software Science and Computation Structure, FoSSaCS'98, Lect. Notes in Comput. Sci. 1378. Springer, pp. 48–62, doi:10.1007/BFb0053541.
  10. Thorsten Altenkirch & Nils Anders Danielsson (2010): Termination Checking in the Presence of Nested Inductive and Coinductive Types. Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, FLoC 2010. Available at http://www.cse.chalmers.se/~nad/publications/altenkirch-danielsson-par2010.pdf.
  11. Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh & Nicolas Oury (2010): PiSigma: Dependent Types without the Sugar. In: Matthias Blume, Naoki Kobayashi & Germán Vidal: Proc. of the 10th Int. Symp. on Functional and Logic Programming, FLOPS 2010, Lect. Notes in Comput. Sci. 6009. Springer, pp. 40–55, doi:10.1007/978-3-642-12251-4_5.
  12. Thorsten Altenkirch, Conor McBride & Wouter Swierstra (2007): Observational equality, now!. In: Aaron Stump & Hongwei Xi: Proc. of the Wksh. Programming Languages meets Program Verification, PLPV 2007. ACM Press, pp. 57–68, doi:10.1145/1292597.1292608.
  13. Peter Aczel & Michael Rathjen (2008): Notes on Constructive Set Theory. Available at http://www.maths.manchester.ac.uk/logic/mathlogaps/workshop/CST-book-June-08.pdf. Draft..
  14. Bruno Barras (1999): Auto-validation d'un système de preuves avec familles inductives. Ph.D. thesis. Université Paris 7.
  15. Bruno Barras (2010): Sets in Coq, Coq in Sets. J. Formalized Reasoning 3(1). Available at http://jfr.cib.unibo.it/article/view/1695.
  16. Bruno Barras (2010): The syntactic guard condition of Coq. Talk at the Journée ``égalité et terminaison'' du 2 février 2010 in conjunction with JFLA 2010. Available at http://coq.inria.fr/files/adt-2fev10-barras.pdf.
  17. Bruno Barras & Bruno Bernardo (2008): The Implicit Calculus of Constructions as a Programming Language with Dependent Types. In: Roberto M. Amadio: FoSSaCS, Lect. Notes in Comput. Sci. 4962. Springer, pp. 365–379, doi:10.1007/978-3-540-78499-9_26.
  18. Gilles Barthe, Benjamin Grégoire & Fernando Pastawski (2006): CIC^: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. In: Miki Hermann & Andrei Voronkov: Proc. of the 13th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2006, Lect. Notes in Comput. Sci. 4246. Springer, pp. 257–271, doi:10.1007/11916277_18.
  19. Gilles Barthe, Benjamin Grégoire & Colin Riba (2008): A Tutorial on Type-Based Termination. In: Ana Bove, Lu\'ıs Soares Barbosa, Alberto Pardo & Jorge Sousa Pinto: LerNet ALFA Summer School, Lect. Notes in Comput. Sci. 5520. Springer, pp. 100–152, doi:10.1007/978-3-642-03153-3_3.
  20. Gilles Barthe, Benjamin Grégoire & Colin Riba (2008): Type-Based Termination with Sized Products. In: Michael Kaminski & Simone Martini: Computer Science Logic, 22nd Int. Wksh., CSL 2008, 17th Annual Conf. of the EACSL, Lect. Notes in Comput. Sci. 5213. Springer, pp. 493–507, doi:10.1007/978-3-540-87531-4_35.
  21. Frédéric Blanqui (2004): A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems. In: Vincent van Oostrom: Rewriting Techniques and Applications (RTA 2004), Aachen, Germany, Lect. Notes in Comput. Sci. 3091. Springer, pp. 24–39, doi:10.1007/978-3-540-25979-4_2.
  22. Patrick Cousot & Radhia Cousot (1979): Constructive Versions of Tarski's Fixed Point Theorems. Pacific Journal of Mathematics 81(1), pp. 43–57.
  23. Gang Chen (1997): Subtyping Calculus of Construction (Extended Abstract). In: Igor Pr\'ıvara & Peter Ruzicka: Proc. of the 22nd Int. Symb. on Mathematical Foundations of Computer Science, MFCS'97, Lect. Notes in Comput. Sci. 1295. Springer, pp. 189–198, doi:10.1007/BFb0029962.
  24. Gang Chen (2003): Coercive subtyping for the calculus of constructions. In: Proc. of the 30st ACM Symp. on Principles of Programming Languages, POPL 2003, ACM SIGPLAN Notices 38. ACM Press, pp. 150–159, doi:10.1145/640128.604145.
  25. Thierry Coquand (1993): Infinite Objects in Type Theory. In: H. Barendregt & T. Nipkow: Types for Proofs and Programs (TYPES '93), Lect. Notes in Comput. Sci. 806. Springer, pp. 62–78, doi:10.1007/3-540-58085-9_72.
  26. Nils Anders Danielsson & Thorsten Altenkirch (2010): Subtyping, Declaratively. In: Claude Bolduc, Jules Desharnais & Béchir Ktari: Proc. of the 10th Int. Conf. on Mathematics of Program Construction, MPC 2010, Lect. Notes in Comput. Sci. 6120. Springer, pp. 100–118, doi:10.1007/978-3-642-13321-3_8.
  27. Mads Dam & Dilian Gurov (2002): μ-Calculus with Explicit Points and Approximations. J. Log. Comput. 12(2), pp. 255–269, doi:10.1093/logcom/12.2.255.
  28. Maria João Frade (2003): Type-Based Termination of Recursive Definitions and Constructor Subtyping in Typed Lambda Calculi. Ph.D. thesis. Universidade do Minho, Departamento de Informática.
  29. Neil Ghani, Peter Hancock & Dirk Pattinson (2006): Continuous Functions on Final Coalgebras. Electr. Notes in Theor. Comp. Sci. 164(1), pp. 141–155, doi:10.1016/j.entcs.2006.06.009.
  30. Neil Ghani, Peter Hancock & Dirk Pattinson (2009): Representations of Stream Processors Using Nested Fixed Points. Logical Meth. in Comput. Sci. 5(3), doi:10.2168/LMCS-5(3:9)2009.
  31. Eduardo Giménez (1995): Codifying Guarded Definitions with Recursive Schemes. In: Peter Dybjer, Bengt Nordström & Jan Smith: Types for Proofs and Programs, Int. Wksh., TYPES'94, Lect. Notes in Comput. Sci. 996. Springer, pp. 39–59, doi:10.1007/3-540-60579-7_3.
  32. Eduardo Giménez (1998): Structural Recursive Definitions in Type Theory. In: K. G. Larsen, S. Skyum & G. Winskel: Int. Colloquium on Automata, Languages and Programming (ICALP'98), Aalborg, Denmark, Lect. Notes in Comput. Sci. 1443. Springer, pp. 397–408, doi:10.1007/BFb0055070.
  33. Jean-Yves Girard (1972): Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur. Thèse de Doctorat d'État. Université de Paris VII.
  34. John Hughes, Lars Pareto & Amr Sabry (1996): Proving the Correctness of Reactive Systems Using Sized Types. In: Proc. of the 23rd ACM Symp. on Principles of Programming Languages, POPL'96, pp. 410–423, doi:10.1145/237721.240882.
  35. DeLesley S. Hutchins (2010): Pure subtype systems. In: Manuel V. Hermenegildo & Jens Palsberg: Proc. of the 37th ACM Symp. on Principles of Programming Languages, POPL 2010. ACM Press, pp. 287–298, doi:10.1145/1706299.1706334.
  36. INRIA (2010): The Coq Proof Assistant Reference Manual, version 8.3 edition. INRIA. Available at http://coq.inria.fr/.
  37. Zhaohui Luo & Robin Adams (2008): Structural subtyping for inductive types with functorial equality rules. Math. Struct. in Comput. Sci. 18(5), pp. 931–972, doi:10.1017/S0960129508006956.
  38. Conor McBride (2009): Let's See How Things Unfold: Reconciling the Infinite with the Intensional. In: Alexander Kurz, Marina Lenisa & Andrzej Tarlecki: 3rd Int. Conf. on Algebra and Coalgebra in Computer Science, CALCO 2009, Lect. Notes in Comput. Sci. 5728. Springer, pp. 113–126, doi:10.1007/978-3-642-03741-2_9.
  39. Nax Paul Mendler (1987): Recursive Types and Type Constraints in Second-Order Lambda Calculus. In: Proc. of the 2nd IEEE Symp. on Logic in Computer Science (LICS'87). IEEE Computer Soc. Press, pp. 30–36.
  40. Robin Milner (1978): A Theory of Type Polymorphism in Programming. J. Comput. Syst. Sci. 17, pp. 348–375, doi:10.1016/0022-0000(78)90014-4.
  41. Ulf Norell (2007): Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. thesis. Dept of Comput. Sci. and Engrg., Chalmers, Göteborg, Sweden.
  42. Lars Pareto (2000): Types for Crash Prevention. Ph.D. thesis. Chalmers University of Technology.
  43. Brigitte Pientka (2001): Termination and Reduction Checking for Higher-Order Logic Programs. In: Rajeev Goré, Alexander Leitsch & Tobias Nipkow: Automated Reasoning, First International Joint Conference, IJCAR 2001, Lect. Notes in Art. Intell. 2083. Springer, pp. 401–415, doi:10.1007/3-540-45744-5_32.
  44. Zhenyu Qian & Tobias Nipkow (1994): Reduction and Unification in Lambda Calculi with a General Notion of Subtype. J. of Autom. Reasoning 12(3), pp. 389–406, doi:10.1007/BF00885767.
  45. John C. Reynolds (1974): Towards a Theory of Type Structure. In: B. Robinet: Programming Symposium, Lect. Notes in Comput. Sci. 19. Springer, Berlin, pp. 408–425, doi:10.1007/3-540-06859-7_148.
  46. Jorge Luis Sacchini (2011): On Type-Based Termination and Pattern Matching in the Calculus of Inductive Constructions. Ph.D. thesis. INRIA Sophia-Antipolis and École des Mines de Paris.
  47. Christoph Sprenger & Mads Dam (2003): On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μ-Calculus. In: Andrew D. Gordon: Proc. of the 6th Int. Conf. on Foundations of Software Science and Computational Structures, FoSSaCS 2003, Lect. Notes in Comput. Sci. 2620. Springer, pp. 425–440, doi:10.1007/3-540-36576-1_27.
  48. Ulrich Schöpp & Alex K. Simpson (2002): Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes. In: Mogens Nielsen & Uffe Engberg: Proc. of the 5th Int. Conf. on Foundations of Software Science and Computational Structures, FoSSaCS 2002, Lect. Notes in Comput. Sci. 2303. Springer, pp. 372–386, doi:10.1007/3-540-45931-6_26.
  49. Martin Steffen (1998): Polarized Higher-Order Subtyping. Ph.D. thesis. Technische Fakultät, Universität Erlangen.
  50. William W. Tait (1967): Intensional Interpretations of Functionals of Finite Type I. J. Symb. Logic 32(2), pp. 198–212.
  51. David Wahlstedt (2000): Detecting termination using size-change in parameter values. Master's thesis. Göteborgs Universitet.
  52. Hongwei Xi (2002): Dependent Types for Program Termination Verification. J. Higher-Order and Symb. Comput. 15(1), pp. 91–131, doi:10.1023/A:1019916231463.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org