User loginNavigation |
archivesReasoning 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. |
Browse archivesActive forum topics
|
Recent comments
11 weeks 1 day ago
15 weeks 3 days ago
17 weeks 11 hours ago
17 weeks 11 hours ago
19 weeks 5 days ago
24 weeks 2 days ago
24 weeks 2 days ago
24 weeks 5 days ago
24 weeks 5 days ago
27 weeks 4 days ago