<feed xmlns='http://www.w3.org/2005/Atom'>
<title>aeneas/.gitignore, 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>
<entry>
<title>Add simple test runner</title>
<updated>2024-05-24T12:24:38+00:00</updated>
<author>
<name>Nadrieril</name>
</author>
<published>2024-05-22T13:11:28+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=6f14e8c699169aa11ea9c106f8cae1ba593569d0'/>
<id>6f14e8c699169aa11ea9c106f8cae1ba593569d0</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Ensure `./charon` points to a valid charon clone</title>
<updated>2024-05-14T13:01:39+00:00</updated>
<author>
<name>Nadrieril</name>
</author>
<published>2024-05-03T11:29:27+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=b923f7232a9e98a0b039b722ffedcf91051edbe6'/>
<id>b923f7232a9e98a0b039b722ffedcf91051edbe6</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Update charon pin</title>
<updated>2024-04-18T09:54:39+00:00</updated>
<author>
<name>Nadrieril</name>
</author>
<published>2024-04-08T14:45:27+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=6ef342ea6ceb0a49929859ef96c5e0afcea7451f'/>
<id>6ef342ea6ceb0a49929859ef96c5e0afcea7451f</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Update the HOL4 proofs for the last *release* version of HOL4</title>
<updated>2023-06-04T19:54:38+00:00</updated>
<author>
<name>Son Ho</name>
</author>
<published>2023-06-02T15:23:29+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=dc46dbb9a01329c39673fedc195006745c365030'/>
<id>dc46dbb9a01329c39673fedc195006745c365030</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Make minor modifications</title>
<updated>2023-06-04T19:54:38+00:00</updated>
<author>
<name>Son Ho</name>
</author>
<published>2023-01-23T23:09:33+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=a9110a7fe013dc7b6dd35bfd6f56ea1ce3a471b1'/>
<id>a9110a7fe013dc7b6dd35bfd6f56ea1ce3a471b1</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>New directory structure and corresponding extraction, + misc fixes, for Lean</title>
<updated>2023-06-04T19:44:33+00:00</updated>
<author>
<name>Jonathan Protzenko</name>
</author>
<published>2023-01-25T21:12:01+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=e1ee59f6a45482e93901f6a549f594fd6ef15234'/>
<id>e1ee59f6a45482e93901f6a549f594fd6ef15234</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Make good progress on the Coq backend</title>
<updated>2022-11-14T13:21:04+00:00</updated>
<author>
<name>Son Ho</name>
</author>
<published>2022-11-13T22:00:38+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=fc21cf96f80ccb7e6455c057987bb0ff4597c0bb'/>
<id>fc21cf96f80ccb7e6455c057987bb0ff4597c0bb</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Reorganize the project to prepare for new backends</title>
<updated>2022-11-14T13:21:04+00:00</updated>
<author>
<name>Son Ho</name>
</author>
<published>2022-11-11T20:34:29+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=6db835db88c4bcf0e00ce1a7a6bc396382b393c3'/>
<id>6db835db88c4bcf0e00ce1a7a6bc396382b393c3</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
<entry>
<title>Update the .gitignore</title>
<updated>2022-11-11T14:26:17+00:00</updated>
<author>
<name>Son Ho</name>
</author>
<published>2022-11-11T14:10:57+00:00</published>
<link rel='alternate' type='text/html' href='https://stuebinm.eu/git/aeneas/commit/?id=2ad6fec65b0d591da3a2831d4e2c7443f7a22673'/>
<id>2ad6fec65b0d591da3a2831d4e2c7443f7a22673</id>
<content type='text'>
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
</pre>
</div>
</content>
</entry>
</feed>
