Posts by mudri@mathstodon.xyz
 (DIR) Post #AbJu5g9EhQ0adPqWUi by mudri@mathstodon.xyz
       2023-10-30T21:21:38Z
       
       0 likes, 1 repeats
       
       It's been a while coming, but I formally submitted my PhD thesis earlier today.A Framework for Semiring-Annotated Type Systemshttps://personal.cis.strath.ac.uk/james.wood.100/pub/thesis.pdfAbstract:The use of proof assistants as a tool for programming language theorists is becoming ever more practical and widespread. There is a range of satisfactory implementations of simply typed calculi in proof assistants based on dependent type theory.In this thesis, I extend an account of Simply Typed λ-calculus so as to be able to represent and reason about calculi whose variables have restricted usage patterns. Examples of such calculi include a logic with an S4 □-modality, in which certain variables cannot be used “inside” a box (□); and Linear Logic, in which linear variables have to be used exactly once. While there are existing implementations of some of these calculi in proof assistants, many of these implementations share little with the best presentations of simply typed calculi without variable usage restrictions, and thus end up being poorly understood or suboptimal in facilitating mechanised reasoning.Concretely, the main result of this thesis is a framework for representing and reasoning about a wide range of calculi with restricted variable usage. All of these calculi support novel simultaneous renaming and substitution operations. Furthermore, I provide several other examples of generic and specific programs facilitated by the framework. All of this work is implemented in the proof assistant Agda.
       
 (DIR) Post #Aiz9Tian2Afi3dBDN2 by mudri@mathstodon.xyz
       2024-06-16T06:28:49Z
       
       0 likes, 0 repeats
       
       @demofox @ZachWeinersmith Chinese net migration is only about -300K. Most of the population decrease is natural.
       
 (DIR) Post #B2WfDFcMW0KPjHpyWu by mudri@mathstodon.xyz
       2023-01-15T00:32:10Z
       
       1 likes, 0 repeats
       
       @ColinTheMathmo This phrasing was well enough understood in the UK a few years ago to be part of Theresa May's “just about managing (JAM)” descriptor. https://www.theguardian.com/commentisfree/2016/nov/21/theresa-may-jams-rhetoric-just-managing-families-autumn-statement