Browse thread
Programming with correctness guarantees
-
oleg@p...
- Andrej Bauer
- Joshua D. Guttman
- Jean-Christophe Filliatre
-
David MENTRE
- Benedikt Grundmann
- Kenn Knowles
- Hendrik Tews
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Benedikt Grundmann <benedikt@c...> |
| Subject: | Re: [Caml-list] Design-by-contract and Type inference? |
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 <dmentre@linux-france.org>:
>
> 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 <dmentre@linux-france.org>
> 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
>