Next Sydney PLT meeting is on Tuesday 6th August.

[Ben Lippmeier]

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. 

Venue:

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.

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.

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]

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: https://www.youtube.com/watch?v=ogXlQf8lDD4 . It introduces an alternative to the lambda calculus called 'closure calculus' by Barry Jay (2018).

POPL Paper: https://popl19.sigplan.org/details/pepm-2019-papers/5/A-Simpler-Lambda-Calculus
Slides from the talk:
https://slides.yowconference.com/yowlambdajam2019/XuanyiChew-AnAlienLambdaCalculus.pdf

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

--
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 discus-lang...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/discus-lang/98880AF7-D20A-480D-9576-19BE2D5A11E0%40ouroborus.net.