EDP Sciences logo
Subscriber Authentication Point
Search
Menu
All issues Volume 38 / No 4 (October-December 2004) RAIRO-Theor. Inf. Appl., 38 4 (2004) 277-319 References
Issue
RAIRO-Theor. Inf. Appl.
Volume 38, Number 4, October-December 2004
Fixed Points in Computer Science (FICS'03)
Page(s) 277 - 319
DOI https://doi.org/10.1051/ita:2004015
Published online 15 October 2004
  1. A. Abel, Specification and verification of a formal system for structurally recursive functions, in Types for Proof and Programs, International Workshop, TYPES '99, edited by T. Coquand, P. Dybjer, B. Nordström, J. Smith, Springer. Lect. Notes Comput. Sci. 1956 (2000) 1–20. [CrossRef] [Google Scholar]
  2. A. Abel, A third-order representation of the λµ-calculus, edited by S. Ambler, R. Crole, A. Momigliano, Elsevier Science Publishers. Electron. Notes Theor. Comput. Sci. 58 (2001). [Google Scholar]
  3. A. Abel, Termination and guardedness checking with continuous types, in Typed Lambda Calculi and Applications (TLCA 2003), edited by M. Hofmann, Valencia, Spain, Springer. Lect. Notes Comput. Sci. 2701 (2003) 1–15. [CrossRef] [Google Scholar]
  4. A. Abel, Soundness of a bidirectional typing algorithm. Twelf code, available on the author's homepage, http://www.tcs.informatik.uni-muenchen.de/ abel (May 2004). [Google Scholar]
  5. A. Abel and T. Altenkirch, A predicative analysis of structural recursion. J. Funct. Programming 12 (2002) 1–41. [MathSciNet] [Google Scholar]
  6. T. Altenkirch, Constructions, Inductive Types and Strong Normalization. Ph.D. Thesis, University of Edinburgh (Nov. 1993). [Google Scholar]
  7. R.M. Amadio and S. Coupet-Grimal, Analysis of a guard condition in type theory, in Foundations of Software Science and Computation Structures, First International Conference, FoSSaCS'98, edited by M. Nivat, Springer. Lect. Notes Comput. Sci. 1378 (1998). [Google Scholar]
  8. T. Arts and J. Giesl, Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236 (2000) 133–178. [CrossRef] [Google Scholar]
  9. G. Barthe, M.J. Frade, E. Giménez, L. Pinto and T. Uustalu, Type-based termination of recursive definitions. Math. Struct. Comput. Sci. 14 (2004) 1–45. [Google Scholar]
  10. G.M. Bierman, A computational interpretation of the λµ-calculus, in Proc. of Symposium on Mathematical Foundations of Computer Science, edited by L. Brim, J. Gruska, J. Zlatuska, Brno, Czech Republic. Lect. Notes Comput. Sci. 1450 (1998) 336–345. [CrossRef] [Google Scholar]
  11. F. Blanqui, Type Theory and Rewriting. Ph.D. Thesis, Université Paris XI (Sept. 2001). [Google Scholar]
  12. F. Blanqui, A type-based termination criterion for dependently-typed higher-order rewrite systems, in 15th International Conference on Rewriting Techniques and Applications (RTA 04), June 3–5, 2004, Aachen, Germany, Springer. Lect. Notes Comput. Sci. 3091 (2004) 24–39. [CrossRef] [Google Scholar]
  13. F. Blanqui, J.-P. Jouannaud and M. Okada, Inductive data type systems. Theor. Comput. Sci. 277 (2001). [Google Scholar]
  14. J. Brauburger and J. Giesl, Termination analysis for partial functions, in Proc. of the Third International Static Analysis Symposium (SAS'96), Aachen, Germany, Springer. Lect. Notes Comput. Sci. 1145 (1996). [Google Scholar]
  15. W.-N. Chin and S.-C. Khoo, Calculating sized types. Higher-Order and Symbolic Computation 14 (2001) 261–300. [CrossRef] [Google Scholar]
  16. C. Coquand, Agda. WWW page (2000) http://www.cs.chalmers.se/ catarina/agda/ [Google Scholar]
  17. T. Coquand, Infinite objects in type theory, in Types for Proofs and Programs (TYPES '93), edited by H. Barendregt, T. Nipkow, Springer. Lect. Notes Comput. Sci. 806 (1993) 62–78. [Google Scholar]
  18. T. Coquand, An algorithm for type-checking dependent types, in Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction, July 17–21, 1995, Kloster Irsee, Germany, Elsevier Science. Sci. Comput. Programming 26 167–177 (1996). [Google Scholar]
  19. K. Crary and S. Weirich, Resource bound certification, in Proc. of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, Massachusetts, USA (Jan. 2000) 184–198. [Google Scholar]
  20. R. Davies and F. Pfenning, Intersection types and computational effects, in Proc. of the International Conference on Functional Programming (ICFP 2000), Montreal, Canada (Sept. 2000) 198–208. [Google Scholar]
  21. J. Dunfield and F. Pfenning, Tridirectional typechecking, in 31st Annual Symposium on Principles of Programming Languages (POPL'04), edited by N.D. Jones and X. Leroy, Venice, Italy. ACM (Jan. 2004) 281–292. [Google Scholar]
  22. J. Giesl, Termination of nested and mutually recursive algorithms. J. Automat. Reason. 19 (1997) 1–29. [CrossRef] [MathSciNet] [Google Scholar]
  23. E. Giménez, Structural recursive definitions in type theory, in Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 13–17 1998, Proc., Springer. Lect. Notes Comput. Sci. 1443 (1998) 397–408. [CrossRef] [Google Scholar]
  24. C. Haack and J.B. Wells, Type error slicing in implicitly typed, higher-order languages, in Programming Languages and Systems, 12th European Symp. Programming, Springer. Lect. Notes Comput. Sci. 2618 (2003) 284–301. [CrossRef] [Google Scholar]
  25. T. Hagino, A typed lambda calculus with categorical type constructors, in Category Theory and Computer Science, edited by D.H. Pitt, A. Poigné, D.E. Rydeheard. Lect. Notes Comput. Sci. 283 (1987) 140–157. [Google Scholar]
  26. T. Hallgren, Alfa home page. http://www.math.chalmers.se/ hallgren/Alfa/ (2003). [Google Scholar]
  27. J. Hughes and L. Pareto, Recursion and dynamic data-structures in bounded space: Towards embedded ML programming, in International Conference on Functional Programming (ICFP'99) (1999) 70–81. [Google Scholar]
  28. J. Hughes, L. Pareto and A. Sabry, Proving the correctness of reactive systems using sized types, in Symposium on Principles of Programming Languages (1996) 410–423. [Google Scholar]
  29. INRIA, The Coq Proof Assistant Reference Manual, version 8.0 edition (April 2004). http://coq.inria.fr/doc/main.html [Google Scholar]
  30. C.S. Lee, N.D. Jones and A.M. Ben-Amram, The size-change principle for program termination, in ACM Symposium on Principles of Programming Languages (POPL'01), London, UK. ACM Press (Jan. 2001). [Google Scholar]
  31. Z. Luo, ECC: An Extended Calculus of Constructions. Ph.D. Thesis, University of Edinburgh (1990). [Google Scholar]
  32. R. Matthes, Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. Thesis, Ludwig-Maximilians-University (May 1998). [Google Scholar]
  33. C. McBride, Dependently Typed Functional Programs and their Proofs. Ph.D. Thesis, University of Edinburgh (1999). [Google Scholar]
  34. N.P. Mendler, Recursive types and type constraints in second-order lambda calculus, in Proc. of the Second Annual IEEE Symposium on Logic in Computer Science, Ithaca, New York. IEEE Computer Society Press (1987) 30–36. [Google Scholar]
  35. N.P. Mendler, Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Logic 51 (1991) 159–172. [CrossRef] [MathSciNet] [Google Scholar]
  36. R. Milner, A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17 (1978) 348–375. [Google Scholar]
  37. L. Pareto, Types for Crash Prevention. Ph.D. Thesis, Chalmers University of Technology (2000). [Google Scholar]
  38. M. Parigot, λµ-calculus: An algorithmic interpretation of classical natural deduction, in Logic Programming and Automated Reasoning: Proc. of the International Conference LPAR'92, edited by A. Voronkov, Springer, Berlin, Heidelberg (1992) 190–201. [Google Scholar]
  39. F. Pfenning and C. Schürmann, System description: Twelf – a meta-logical framework for deductive systems, in Proc. of the 16th International Conference on Automated Deduction (CADE-16), edited by H. Ganzinger, Springer, Trento, Italy. Lect. Notes Artif. Intell. 1632 (1999) 202–206. [Google Scholar]
  40. B. Pientka, Termination and reduction checking for higher-order logic programs, in Automated Reasoning, First International Joint Conference, IJCAR 2001, edited by R. Goré, A. Leitsch, and T. Nipkow, Springer. Lect. Notes Artif. Intell. 2083 (2001) 401–415. [Google Scholar]
  41. B.C. Pierce, Types and Programming Languages. MIT Press (2002). [Google Scholar]
  42. B.C. Pierce, D.N. Turner, Local type inference, in POPL 98: The 25TH ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California (1998). [Google Scholar]
  43. R. Pollack, The Theory of LEGO. Ph.D. Thesis, University of Edinburgh (1994). [Google Scholar]
  44. Z. Spławski and P. Urzyczyn, Type fixpoints: Iteration vs. recursion, in Proc. of the 1999 International Conference on Functional Programming (ICFP), Paris, France. SIGPLAN Notices 34 (1999) 102–113. [CrossRef] [Google Scholar]
  45. A.J. Telford and D.A. Turner, Ensuring streams flow, in Algebraic Methodology and Software Technology (AMAST '97), Springer. Lect. Notes Comput. Sci. 1349 (1997) 509–523. [CrossRef] [Google Scholar]
  46. A.J. Telford and D.A. Turner, Ensuring termination in ESFP, in Proc. of BCTCS 15, 1999. J. Universal Comput. Sci. 6 (2000) 474–488. [Google Scholar]
  47. T. Uustalu and V. Vene, Primitive (co)recursion and course-of-value (co)iteration, categorically. Informatica (Lithuanian Academy of Sciences) 10 (1999) 5–26. [Google Scholar]
  48. C. Walther, Argument-Bounded Algorithms as a Basis for Automated Termination Proofs, in 9th International Conference on Automated Deduction, edited by E.L. Lusk and R.A. Overbeek, Springer. Lect. Notes Comput. Sci. 310 (1988) 602–621. [CrossRef] [Google Scholar]
  49. A.K. Wright and M. Felleisen, A syntactic approach to type soundness. Inform. Comput. 115 (1994) 38–94. [CrossRef] [Google Scholar]
  50. H. Xi, Dependent types for program termination verification. J. Higher-Order and Symbolic Computation 15 (2002) 91–131. [CrossRef] [Google Scholar]
  51. J. Yang, G. Michaelson and P. Trinder, Explaining polymorphic types. Comput. J. 45 (2002) 436–452. [CrossRef] [Google Scholar]

Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.

Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.

Initial download of the metrics may take a while.