amosr
postdoc at ANU, interested in programming languages and critical systems
Australian National UniversitySydney, Australia
Pinned Repositories
clustering
implementation of clustering/scheduling for combinators, using ILP
clustering-proof
Coq proofs of validity of ILP clustering algorithm
coq
folderol
machine fusion
game-jet
game-pilot
limp
ideally, this will become a pure Haskell library for Linear Integer/Mixed Programming
limp-cbc
Coin-OR/CBC bindings for Haskell
papers
amosr's Repositories
amosr/folderol
machine fusion
amosr/limp
ideally, this will become a pure Haskell library for Linear Integer/Mixed Programming
amosr/limp-cbc
Coin-OR/CBC bindings for Haskell
amosr/clustering
implementation of clustering/scheduling for combinators, using ILP
amosr/coq
amosr/game-pilot
amosr/papers
amosr/clustering-proof
Coq proofs of validity of ILP clustering algorithm
amosr/game-jet
amosr/nominal-wyvern
Nominal Wyvern typechecker for subtyping decidability
amosr/phd
papers for lit review
amosr/streamtiling
'Controlled' stream fusion
amosr/CompCert
The CompCert formally-verified C compiler
amosr/ddc
The Disciplined Disciple Compiler
amosr/frama_c_example
A small example using Frama-C example
amosr/FStar
A Proof-oriented Programming Language
amosr/fstar-vscode-assistant
An interactive mode for F* in VS Code
amosr/icicle
A streaming query language.
amosr/isa-value-parser
Simple, faster parser for "value terms" in Isabelle.
amosr/karamel
KaRaMeL is a tool for extracting low-level F* programs to readable C code
amosr/kind2
Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
amosr/merges
playing around with merges
amosr/monad-free
how do you write hedgehog without monads
amosr/pulse
The Pulse separation logic DSL for F*
amosr/squealing-funicular
amosr/talks
talks
amosr/thesis
please disregard
amosr/velus
A Lustre compiler in Coq
amosr/website
amosr/xylo
Xylophone and idiophone experiments