Next Sydney PLT Meeting is on Tuesday 10th September

[Ben Lippmeier]

Various programming languages diaspora are meeting monthly on Tuesday evenings, two weeks after FP-Syd. This is an informal gathering and discussion without pre-prepared talks. All interested parties are welcome. 

Venue:

The Local Taphouse

122 Flinders St, Darlinghurst NSW 2010
6:30pm Tuesday, 10th September 2019

If you arrive and can’t find us then call Ben Lippmeier +61 421 381 880.

Cheers,

Ben.

Current projects include:

Tako: An experimental programming language for ergonomic software verification using Hoare Logic. https://github.com/Cypher1/tako

Salt: The compilation target that functional programmers always wanted. Salt is what you get when you leave C out in the sun for too long. Now comes with a partially baked VSCode language server plugin. Repo is at https://github.com/discus-lang/salt

Discus: An experimental dialect of Haskell that investigates static typing and program transformation in the presence of computational effects. DDC is the compiler for it. More info at http://discus-lang.org/

Accelerate: An embedded language for accelerated array processing on GPGPUs. More info at http://hackage.haskell.org/package/accelerate.

If any of the attendees have another project they want publicised then reply to this mail, or let me know for next month and I’ll include it.

[Ben Lippmeier]

On 5 Sep 2019, at 3:36 pm, Ben Lippmeier <be...@ouroborus.net> wrote:

Various programming languages diaspora are meeting monthly on Tuesday evenings, two weeks after FP-Syd. This is an informal gathering and discussion without pre-prepared talks. All interested parties are welcome. 

Venue:

The Local Taphouse

122 Flinders St, Darlinghurst NSW 2010
6:30pm Tuesday, 10th September 2019

Notes from meeting 10/9/2019

Attendees (4): Erik, Josh M, Richard, Ben.

Ben and Josh attended ICFP in Berlin. Notable papers: Agda extension for Cubical Type Theory. Typed Holes in GHC. Lennart Augustsson and Satnam Singh gave a good talk about use of GHC/Haskell in their project at X. Several groups are now looking at verifying properties of neural networks.

Next year’s ICFP is in New Jersey, then Seoul in 2021, then Slovenia in 2022.

Erik: working on the backend for the Cardano block explorer. Has had good experiences with the persistent and esqueleto Haskell libraries.

Josh: working on extensible .hi files for GHC, so more information can be stored in them to aid cross compilation. 

Josh: went to the Cardano meetup while Berlin. Showed a ‘Tangem’ crypto wallet card that holds the private key in a secure IC and can be used to sign transactions. The private key cannot be retrieved from the hardware without destroying the IC. To perform transactions one can simply give someone else the card.

Erik: private transactions are now increasingly being done using Monero instead of the other currencies. US agencies have been blacklisting certain Bitcoin(etc) addresses and exchanges will not take any coins that have been coin joined with the blacklisted coins. Bitcoins ‘pseudo anonymity’ has ceased being good enough for private transactions.

Ben: has been testing out the Why3 prover framework for proving properties about image processing algorithms. Programs are written in a simple dialect of ML called WhyML, which includes preconditions and postconditions for functions (using the ‘requires’ and ‘ensures’ keyword). Intermediate verification goals can be farmed out to a range of SMT solvers including Alt-Ergo, CVC4 and Z3. The experience has been good so far. The framework uses first order logic so one cannot parameterise properties by other properties, but the SMT solvers are good at handling the sort of statements about array indexing you get when verifying image processing algorithms.

Notes from earlier meeting of 6/8/2019

Attendees (4): Amos, Erik, Richard, Ben.

Richard / Amos: have been reading about Barry’s Closure Calculus (from the paper A Simpler Lambda Calculus). Amos did a formalisation in Isabelle and agrees that it’s easier to formalises than lambda calculi using traditional approaches to substitution.

Erik: writing a blockchain explorer for Cardano. The backend uses Postgres domain types to help ensure the data stays well formed. The domain types are like static refinement types, except they are checked at runtime.

Erik: mentions Zether, a new mechanism for performing private transactions on the main Ethereum blockchain.

Ben: joined Ghost Locomotion along with Amos, Tran and Kai. Have been reading about SPIR language for GPGPU programming, and writing some simple examples in OpenCL to get familiar with the API. Also reading about the various weak memory models exposed by OpenCL and other languages.

Erik: describes fuzz testing of libsndfile using the American Fuzzy Lop fuzz testing framework. Found ~30 bugs in 3-4 days of fuzzing, which is more than have been found in the last 15 years of production use as a well used open source library.

Ben: started reading about verification of neural networks. Amos mentions recent work on placing bounds on the output of a neural network. Propagates bounds backwards using an SMT solver.