@rg9119 Congratulations! That’s thoroughly deserved.

@ah @standefer Once they see the weird five-element Heyting lattice generated by the three-point Kripke frame, scales begin to fall from their eyes.

@ah I second @standefer’s recommendation.

One fun exercise I do after having introduced small Heyting lattices to my undergrad students (which seem like unintelligible mystery boxes) and then Kripke frames, is getting them to construct a few lattice of propositions generated by different small Kripke frames. That helps give them a sense of what is going on.

Whilst I do not like tooting my own horn, if you were interested in my #TYPES2025 talk (Towards Being Positively Negative about Dependent Types) and could not make it.

Here you go:

https://www.youtube.com/watch?v=8xc50Lf6pXs

@pigworker Coauthors who can keep their eye on the ball while enjoying playing the game are worth more than gold.

@pigworker it is so depressing that this is a measure that means too much to the bean counters. But signs of life are good, wherever we can find them.

The recordings from #TYPES2025 are beginning to appear on @mspstrath’s youtube channel. There is a lot of good stuff there already, and I plan to re-watch some talks I enjoyed in the days ahead.

Here is the recording of my talk on some of the connections between type theory and issues in philosophical logic: https://www.youtube.com/watch?v=rlInQX5VJqg

(Although I was shown the general area to stand in so that you are visible to the camera was recording, apparently I resolutely ignored that as I wandered around the room as is my habit when teaching/speaking.)

"We sent the student's draft of his dissertation to an expert in the field, who said the main theorem was too trivial. In fact, it turned out to be incorrect. Although this sounds like the stuff of a joke - not only is this result obvious but it's not true - I think it was probably an accurate appraisal."
Fred Richman

https://web.archive.org/web/20230204213103/http://math.fau.edu/richman/docs/confess.pdf

@BeLazy's Types talk is online (https://www.youtube.com/watch?v=mHRwYT0TrIo), with functoriality, type casts, and a pinch of 2-categories to spice up the mix. Part of a whole day of "hey, what if types were categories", which was full of cool ideas – looking forward to see where this all will go. We're working on a proper pre-print which should be out in a bit, stay tuned!

Here's my TYPES talk, Presheaves on Purpose: https://www.youtube.com/watch?v=5F_sLSxEAnA

Only my voice and my hands are in the video. You'll have to imagine my hair and my purple frock.

Slides: https://msp.cis.strath.ac.uk/types2025/slides/TYPES2025-slides46.pdf

The recordings from #TYPES2025 are beginning to appear on @mspstrath’s youtube channel. There is a lot of good stuff there already, and I plan to re-watch some talks I enjoyed in the days ahead.

Here is the recording of my talk on some of the connections between type theory and issues in philosophical logic: https://www.youtube.com/watch?v=rlInQX5VJqg

(Although I was shown the general area to stand in so that you are visible to the camera was recording, apparently I resolutely ignored that as I wandered around the room as is my habit when teaching/speaking.)

Hi all, since fediphilosophy.org is shutting down, I've decided to take my talents to social.coop

New intro for the new instance:
I'm a Senior Lecturer in Philosophy at Hebrew University in Jerusalem. I research ethics, metaethics, and philosophy of perception.

In my free time I do anti-apartheid, anti-occupation, and (now) anti-genocide activism in Israel/Palestine, where I live. I'm originally from the US (Wisconsin).

#philosophy #academia #activism #introduction #israel #palestine

@pigworker As a relatively new resident of Scotland, I *so* want to read/watch this.

My comedy-thriller drama series (which I shall never write) "St Andrew's Cross" imagines a future independent Scotland as a high technology society that defies international pharmaceutical patents and funds contributions to open-source software. Thus incurring the wrath of corporations and England.

Our short open-access book Types and the Structure of Meaning has been published as a Cambridge Element in Semantics https://www.cambridge.org/core/elements/types-and-the-structure-of-meaning/27C1813D046DADA53FC6A2BEC505E941

written with Stergios Chatzikyriakidis, Eleni Gregoromichelaki and Peter Sutton

#semantics #typetheory #linguistics

Last week was all type theory, all the time. *This* week I get to change gears, and take part in the 50th Annual Conference of the Society for Exact Philosophy. I’m especially looking forward to Day 2, which is devoted to the work of our sorely-missed colleague, Aldo Antonelli, who passed away all too soon, ten years ago.

https://meta.phil.ufl.edu/host/sep/meeting.html

@Andrev well, it’s a good and natural idea to socialise the means of computation.

I’ll be giving a talk on the methodology of formal philosophy.

If you want to get a sense of what I’m talking about, details of the talk can be found here: https://consequently.org/presentation/2025/must-do-mdb-better-sep/

Aldo and I served on the editorial board of the Journal of Philosophical Logic, and then the Review of Symbolic Logic. I learned a great deal from him, and from my co-editors, and it will be good to remember him with friends, old and new.

Last week was all type theory, all the time. *This* week I get to change gears, and take part in the 50th Annual Conference of the Society for Exact Philosophy. I’m especially looking forward to Day 2, which is devoted to the work of our sorely-missed colleague, Aldo Antonelli, who passed away all too soon, ten years ago.

https://meta.phil.ufl.edu/host/sep/meeting.html