Top 1K Features Creators Events Podcasts Books Extensions Interviews Blog Explorer CSV

Low*

< >

Low* is a programming language created in 2008.

#2259on PLDB 16Years Old
Homepage


Example from the web:
let chacha20 (len: uint32{len ≤ blocklen}) (output: bytes{len = output.length}) (key: keyBytes) (nonce: nonceBytes{disjoint [output; key; nonce]}) (counter: uint32) : Stack unit (requires (λ m0 → output ∈ m0 ∧ key ∈ m0 ∧ nonce ∈ m0)) (ensures (λ m0 _m1 → modifies1 output m0 m1 ∧ m1.[output] == Seq.prefix len (Spec.chacha20 m0.[key] m0.[nonce]) counter))) = push_frame (); let state = Buffer.create 0ul 32ul in let block = Buffer.sub state 16ul 16ul in chacha20_init block key nonce counter; chacha20_update output state len; pop_frame ()
View source
- Build the next great programming language · About · Search · Keywords · Livestreams · Labs · Resources · Acknowledgements · Part of the World Wide Scroll