<feed xmlns='http://www.w3.org/2005/Atom'>
<title>aeneas/backends/IsabelleHOL/document, branch isabelle</title>
<subtitle>aeneas rust verifier with a hacky Isabelle backend
</subtitle>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/'/>
<entry>
<title>had some fun writing an IsabelleHOL backend</title>
<updated>2024-06-29T20:11:04+00:00</updated>
<author>
<name>stuebinm</name>
</author>
<published>2024-06-29T19:31:22+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=59214186b817329342d9d72e23adf12f7a3b1348'/>
<id>59214186b817329342d9d72e23adf12f7a3b1348</id>
<content type='text'>
(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)
</pre>
</div>
</content>
</entry>
</feed>
