Hey people: please, when you use agda--categories, don't just link to it, cite the paper! Proper academic credit is important, and citations are the way you do it. Maybe in the future, links to github repos will count as citations, but right now they don't.
I've see two recent papers on the arxiv which could be thus 'augmented'. I won't @ the authors (yet?)
I'm speaking at a conference next month. It's been a while. What happens?
Anyway, I see lots of my internet friends will be there too. I'm looking forward to venturing out further than I've been for a long time!
https://www.causalislands.com/sessions/idris-2-quantitative-types-in-action
We have a week off teaching so I get to do some research and some hacking on Idris. So far this week I've done exactly one thing, which is changing a "True" to a "False".
It only took three days to work that out...
(Next step, change the Boolean to something informative. Might be done by next Christmas.)
Hello, world! We are the Programming Languages group at TU Delft. Our current members on Mastodon are @casperbp, @dennis, @virtlink, @liesnikov, @baboum, @casvdrest, @pdmosses, and @agdakx. Stay tuned to this channel to hear all the latest updates from Delft about #Spoofax, #Agda, #TypeTheory, #ModularLanguages, #WeakMemoryModels, and #ProgrammingLanguages in general. #introduction
Now imagining that the questions in the Voight-Kampff test are "Are you a robot?" then "Please point at the traffic lights".
i just realized that there is an entire generation of e-mail users who use the word "CC" and have no idea what it means.
Carbon Copy was a process used to make identical copies of writing (or typewriting) through one or more pieces of paper. it involved using a sheet of thin carbon paper in between two pieces of paper - as you wrote/typed on the top sheet, the carbon would imprint on the bottom sheet using pencil/pen pressure alone.
in the below image, the yellow sheet is the top sheet that you write on - there is a black sheet of carbon paper beneath it - and then a pink sheet that receives the copy below it. the customer gets the yellow sheet, the restaurant keeps the pink sheet.
Regretfully, the petition to remove #LGBT content from the #UK curriculum has 197,100 signatures.
The counter petition asking for that content to remain, is rapidly gaining ground. It now has 78,919 signatures!
Pls sign the counter petition if able. British citizens & UK residents have the right to sign. Pls boost otherwise!
Link to official petition to UK Gov & Parliament: Do not remove LGBT content from the Relationships Education curriculum
Type-Theory as a Language Workbench (EVCS 2023)
@gallais, @edwinb, and I received the word 'unconditionalised' yesterday.
Our paper, submitted to Eelco Visser Commemorative Symposium was fully accepted.
Sad, but happy.
A link to the github (containing source + paper) is available:
https://github.com/jfdm/velo-lang
ArXiV version coming soon.
DOI'd artifact is https://doi.org/10.5281/zenodo.7573031
The new Idris core has finally successfully compiled some code and so @gallais and I have had a celebratory pint or few. I'd try to check the prelude but I'm too scared tonight... Maybe tomorrow.
Anyway, it's January 25th, so by law I have to go and eat haggis now.
Just went to pick up a ticket to see @brianbilston in a couple of weeks. I'm looking forward to seeing how he maintains his anonymity. I'm imagining a paper bag with eye holes and so I'll be disappointed with anything else.
*The C Type System Has Entered the Chat* (one for @edwinb ) https://universeodon.com/@desertfrogger/109657308288525357
Reader in Computer Science at the University of St Andrews. Idris developer, trying to make fancy type systems that are usable and efficient. Occasional Go player. Cricket watcher. Trainee Adult. Will play ukulele for free, will stop for money.