Can I find the talk somewhere?

ajrouvoet commented 7 years ago

Looking at the code in this repository I'd love to hear your talk. Do you know if it has been recorded at the meeting? Or, if that's not the case, do you maybe have some additional notes that could help understand the ideas, implementation and the limitations of what's in this repository?

Thank you in advance.

UlfNorell commented 7 years ago

No recordings and the notes are all in my head. I'd be happy to answer questions though.

Some limitations:

Only Int64 -> Int64 -> Int64 functions.
Very limited instruction set
No nested loops (but I think that would be straightforward to add)
No heap

The aim I had when starting this was to have all proof obligations discharged automatically (the only thing you have to fill in manually is loop invariants). Thus the representation of the machine state is very symbolic, allowing the Agda type checker do a lot of computation over it.

ajrouvoet commented 7 years ago

Thank you for the response. I don't have any concrete questions at the moment.

It's a shame that the AIM talks aren't recorded. Not sure if this the right place, but maybe this can be considered for it's next iteration?

UlfNorell / x86-agda

Can I find the talk somewhere? #1