Hello Well a lot of the stuff you express with DBC can be expressed using dependent types (Array indices are a popular example). You should take that in account in your search for papers (If I recall correctly there are quite a few papers on combining dependent types and (at the very least partial/local) type inference). Cheers, Bene 2007/2/4, David MENTRE : > > Hello Oleg, > > oleg@pobox.com writes: > > > @Book{ barnes-high, > > author = "John Barnes", > > title = "High Integrity Software: > > The {SPARK} Approach to Safety and Security", > [...] > > @TechReport{ hunt-singularity, > > author = "Galen Hunt and James R. Larus and Mart{\'\i}n Abadi and > > Mark Aiken and Paul Barham and Manuel F{\"a}hndrich and > > Chris Hawblitzel and Orion Hodson and Steven Levi and > > Nick Murphy and Bjarne Steensgaard and David Tarditi and > > Ted Wobber and Brian D. Zill", > > title = "An Overview of the {S}ingularity Project", > > Thank you for those interesting pointers. Interestingly both Spark > language and Sing# language used in Singularity contains > Design-by-Contract-like features (pre- and post-conditions, invariants, > ...). > > Does anybody know if there is research on design-by-contract (as used in > Eiffel or Spark) and type inference (as used in OCaml)? For example, > relationships between both mechanisms, how the compiler could infer > contracts for a sub-class of a class, how contracts can be maintained > with minimal work from the programmer (a very useful property of ML type > inference), how contract can be statically checked using type inference > information, etc. > > Best wishes, > d. > -- > GPG/PGP key: A3AD7A2A David MENTRE > 5996 CC46 4612 9CA4 3562 D7AC 6C67 9E96 A3AD 7A2A > > _______________________________________________ > Caml-list mailing list. Subscription management: > http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs >