The core is done, just trying to elaborate 'up' to a concrete syntax.

Trying to finalise concrete syntax for a toy imperative language. Family-styles are hard to decide from: Can the void comment on good/bad practices for concrete syntax design in this space?

re: Apreciation of Imperative Languages ;-)

They did miss an opportunity with the name of their macro creation syntax. I feel it should have been macros_rule ! rather than macro_rules ! but I am not a macro fan, but I imagine those that are are a bit sad...

Apreciation of Imperative Languages ;-)

Learning a bit o' Rust. It seems to blend imperative and functional nicely for its design space. Not all of it I agree with but that like all languages. You like some parts, but not others. Nothing is perfect.

Should PLDI join PACM-PL? Fill out this survey. blog.sigplan.org/2022/06/10/su

I’ve been blogging a bit more recently. It’s been quite good at helping me unload research thoughts out my head. I’m not too worried about the quality, more If I’m miss judging their worth. Are these things that should be followed through and written up for the beans? Not mentioning other side projects… My heart says yes, but my todos for the main research say otherwise…

**New Blog Post**: Follow the Trail! Visualising Bi-Directional Type-Checking as Network Communication.

jfdm.github.io/post/2022-06-08

New Blog Post: Being Positively Negative.

jfdm.github.io/post/2022-06-02

@joey defining everything as Unicode and never telling you what that symbol is called or how to type is, excellent user experience /s

I have written this (using dependent types to reason about the structure of a HDL) up as a blog post.

jfdm.github.io/post/2022-05-25

I suppose this could be turned into a JFP pearl if I expand upon the other things...

For context, for many cases Dec : Type -> Type is fine, but for writing interactive systems it is not. One needs DecInfo : (e,p : Type) -> Type to report why things failed & retain positive proof.

Urgh, that moment when you realise ALL your predicates are not-error-message generating.

The APLAS'22 Artifact Evaluation Committee is looking for reviewers to join us in bettering the quality of research in our field.

If you want to be involved with examining state-of-the-art research then please apply!

2022.splashcon.org/track/aplas

One benefit of shifting init.el to org mode is :tangle no. Let's me swap out sub-configs easily. Which meant I could switch from popwin to popper; popwin wasn't popping for me.

Mastodon has a verification mechanism, though it looks different from Twitter's. We do not ask for your documents. Instead, if you have a website that you are known by, you can verify that you are the owner of that website.

Link to your Mastodon profile from the website, either through a visible link, or through a <link> tag in the head of the document, with a rel=me attribute, and link back to that page from your Mastodon profile. It should then get a green checkmark, like @Mastodon.

Finally, added the Soundness Check to an orchestration language of mine. Tempting as it is to go for the proof, working with graphs is not my forte.

/me ponders how much of a pattern this is:


data Tag : (this,that : Type)
-> (val : that)
-> Type
where
T : (thisVal : thisTy)
-> Tag thisTy thatTy thatVal


It sits between a pair and dependent pair. There is a pairing of two unrelated values...

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.