Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Reasoning with inductive types
18 views
Skip to first unread message
Helmut
Mar 8, 2012, 3:23:11 PM3/8/12
to
Modern Eiffel is a new language which is syntactically based on Eiffel
but has a lot of concepts of functional languages like Haskell, OCaml
or Coq. Modern Eiffel puts the emphasis on static verification, i.e. a
compiler can statically check that a programm written in Modern Eiffel
meets its specification.
The following article http://softwareverificaton.wordpress.com/2012/03/08/76
describes how Modern Eiffel's proof engine can be used to reason about
inductive types. Reasoning is basic on induction.
but has a lot of concepts of functional languages like Haskell, OCaml
or Coq. Modern Eiffel puts the emphasis on static verification, i.e. a
compiler can statically check that a programm written in Modern Eiffel
meets its specification.
The following article http://softwareverificaton.wordpress.com/2012/03/08/76
describes how Modern Eiffel's proof engine can be used to reason about
inductive types. Reasoning is basic on induction.
0 new messages