Next Sydney PLT meeting is on Tuesday 6th August.

Skip to first unread message

Ben Lippmeier

Aug 4, 2019, 6:54:18 AM8/4/19
Note that we’ve moved the meeting half an hour earlier to 6:30pm.

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. 

The Local Taphouse
122 Flinders St, Darlinghurst NSW 2010
6:30pm Tuesday, 6th August 2019

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


Current projects include:

Tako: An experimental programming language for ergonomic software verification using Hoare Logic.

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

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

Accelerate: An embedded language for accelerated array processing on GPGPUs. More info at

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.

Notes from last meeting:

Attendees (6): Amos, Erik, Josh M, Josh P, Tran, Ben

Josh P: discussion of the Tako project he has started, which does Hoare logic style verification. 

Amos: mentions Autocorres which was built as part of the seL4 project. AutoCorres takes C code that uses fixed width ints and tries to lift it to use unbounded Nats, which can make the proof easier. Also simplifies pointer arithmetic.

Josh P: mentions Coherent Extrapolated Volition as part of a conversation about AI risk. CEV seeks to instruct the AI model to “do what I want, not what I tell you”.

Amos: mentions the local organisation Gradient Institute which investigates AI risk locally in Sydney.

Erik: mentions Project Veritas whistleblowing organisation, which investigates issues like ML algorithms that are set up in a way to achieve particular political outcomes.

Josh P: mentions Synquid program synthesiser based on refinement types, a MIT project.

Amos: experimenting with program generation via tactics, trying to get Coq tactics to generate a desired computational program from its type.

Joshua Pratt

Aug 4, 2019, 7:35:43 PM8/4/19
I'm hoping to be there tomorrow, but in case I'm not (and to give others an opportunity to watch it), here's a talk that I found quite interesting: . It introduces an alternative to the lambda calculus called 'closure calculus' by Barry Jay (2018).

POPL Paper:
Slides from the talk:

Hope this is interesting & maybe helpful, will happily move discussion elsewhere if need be.

You received this message because you are subscribed to the Google Groups "Discus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
To view this discussion on the web visit
Reply all
Reply to author
0 new messages