Zobrazeno 1 - 6
of 6
pro vyhledávání: '"Lars Noschinski"'
Autor:
Lars Noschinski
Publikováno v:
Mathematics in Computer Science. 9:23-39
In contrast to other areas of mathematics such as calculus, number theory or probability theory, there is currently no standard library for graph theory for the Isabelle/HOL proof assistant. We present a formalization of directed graphs and essential
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2c44527e223555279b0441124e43de81
https://doi.org/10.1007/s11786-014-0183-z
https://doi.org/10.1007/s11786-014-0183-z
Publikováno v:
Journal of Automated Reasoning. 51:27-56
We present a modular framework to analyze the innermost runtime complexity of term rewrite systems automatically. Our method is based on the dependency pair framework for termination analysis. In contrast to previous work, we developed a direct adapt
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::196c147a8bf578d75008f5a0e0054fcb
https://doi.org/10.1007/s10817-013-9277-6
https://doi.org/10.1007/s10817-013-9277-6
Publikováno v:
Haskell
We report on our experience teaching a Haskell-based functional programming course to over 1100 students for two winter terms. The syllabus was organized around selected material from various sources. Throughout the terms, we emphasized correctness t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::629edbc66ffd28a04936c05049bb0f0d
https://doi.org/10.1145/2633357.2633359
https://doi.org/10.1145/2633357.2633359
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319061993
NASA Formal Methods
NASA Formal Methods
Certifying algorithms compute not only an output, but also a witness that certifies the correctness of the output for a particular input. A checker program uses this certificate to ascertain the correctness of the output. Recent work used the verific
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e19658e5a7d0410b5e62310af98d6ffa
https://doi.org/10.1007/978-3-319-06200-6_4
https://doi.org/10.1007/978-3-319-06200-6_4
Autor:
Lars Noschinski
Publikováno v:
Interactive Theorem Proving ISBN: 9783642323461
ITP
ITP
The Girth-Chromatic number theorem is a theorem from graph theory, stating that graphs with arbitrarily large girth and chromatic number exist. We formalize a probabilistic proof of this theorem in the Isabelle/HOL theorem prover, closely following a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::16d25ce5d7eba3c2c2184dfbae044954
https://doi.org/10.1007/978-3-642-32347-8_27
https://doi.org/10.1007/978-3-642-32347-8_27
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642224379
CADE
CADE
We present a modular framework to analyze the innermost runtime complexity of term rewrite systems automatically. Our method is based on the dependency pair framework for termination analysis. In contrast to previous work, we developed a direct adapt
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b0a16f77688d1dd4db5aec98a71f2006
https://doi.org/10.1007/978-3-642-22438-6_32
https://doi.org/10.1007/978-3-642-22438-6_32