Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Hello World

Email Gateway (Aug 23 2022 at 08:46):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m happy to announce the following new AFP-entry.

Hello World
by Cornelius Diekmann and Lars Hupel

In this article, we present a formalization of the well-known
"Hello, World!" code, including a formal framework for
reasoning about IO. Our model is inspired by the handling of IO in
Haskell. We start by formalizing the :earth_africa: and embrace the IO monad
afterwards. Then we present a sample main :: IO (), followed by its
proof of correctness.

More details at https://www.isa-afp.org/entries/Hello_World.html

Enjoy,
René
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC