User loginNavigation |
Reasoning with inductive typesModern 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 describes how Modern Eiffel's proof engine can be used to reason with inductive types. By hbrandl at 2012-03-08 20:32 | LtU Forum | previous forum topic | next forum topic | other blogs | 4150 reads
|
Browse archives
Active forum topics |
Recent comments
16 weeks 1 day ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 5 hours ago
51 weeks 4 days ago
51 weeks 4 days ago