Here are some of my latest thoughts… such as thread-first and loop (•̀ᴗ•́)و

## Typed Lisp, A Primer

Let's explore Lisp's fine-grained type hierarchy!

We begin with a shallow comparison to Haskell, a rapid tour of type theory,
try in vain to defend dynamic approaches, give a somewhat humorous account of history,
note that you've been bamboozled —type's have always been there—,
then go into technical details of some Lisp types, and finally conclude by showing
how *macros permit typing*.

Goals for this article:

- Multiple examples of type constructions in Lisp.
- Comparing Lisp type systems with modern languages, such as Haskell.
- Show how algebraic polymorphic types like
`Pair`

and`Maybe`

can be defined in Lisp. Including heterogeneously typed lists! - Convey a passion for an elegant language.
- Augment Lisp with functional Haskell-like type declarations ;-)

Unless suggested otherwise, the phrase “Lisp” refers to Common Lisp as supported by Emacs Lisp. As such, the resulting discussion is applicable to a number of Lisp dialects —I'm ignoring editing types such as buffers and keymaps, for now.

## Have you ever packaged anything?

Herein I try to make my current doctoral research accessible to the average person: Extending dependently-typed languages to implement module system features in the core language. It's something I can direct my family to, if they're inclined to know what it is I've been doing lately.

The technical matter can be seen at the associated website ─The Next 700 Module Systems─ which includes a poster, slides, and a demo.

Excluding the abstract, this is my thesis proposal in *three minutes* (•̀ᴗ•́)و

## An Interactive Way To C

Do you know what the above program accomplishes? If you do, did you also spot a special edge case?

We aim to present an approach to program proving in C using a minimal Emacs setup so that one may produce literate C programs and be able to prove them correct –or execute them– using a single button press; moreover the output is again in Emacs.

The goal is to learn program proving using the Frama-C tool –without necessarily invoking its gui– by loading the source of this file into Emacs then editing, executing, & proving as you read along. One provides for the formal specification of properties of C programs –e.g., using ACSL– which can then be verified for the implementations using tools that interpret such annotation –e.g., Frama-C invoked from within our Emacs setup.

Read on, and perhaps you'll figure out how to solve the missing `FixMe`

pieces 😉

The intent is for rapid editing and checking. Indeed, the Frama-c gui does not permit editing in the gui, so one must switch between their text editor and the gui. Org mode beginning at the basics is a brief tutorial that covers a lot of Org and, from the get-go, covers “the absolute minimum you need to know about Emacs!”

If anything, this effort can be construed as a gateway into interactive theorem proving such as with Isabelle, Coq, or Agda.

The article *aims* to be self-contained —not even assuming familiarity with any C!

The presentation and examples are largely inspired by

- Gilles Dowek's exquisite text Principles of Programming Languages.

- It is tremendously accessible!
- Allan Blanchard's excellent tutorial Introduction to C Program Proof using Frama-C and its WP Plugin.
Another excellent and succinct tutorial is Virgile Prevosto's ACSL Mini-Tutorial. In contrast, the tutorial ACSL By Example aims to provide a variety of algorithms rendered in ACSL.

There are no solutions since it's too easy to give up and look at the solutions that're nearby. Moreover, I intend to use some of the exercises for a class I'm teaching ;-)

## Graphs are to categories as lists are to monoids

Numbers are the lengths of lists which are the flattenings of trees which are
the spannings of graphs.
Unlike the first three, graphs have *two* underlying types of interest
–the vertices and the edges– and it is getting to grips with this complexity
that we attempt to tackle by considering their ‘algebraic’ counterpart: Categories.

In our exploration of what graphs could possibly be and their relationships to lists are,
we shall *mechanise,* or *implement,* our claims since there will be many details and it is easy
to make mistakes –moreover as a self-learning project, I'd feel more confident to make
**bold** claims when I have a proof assistant checking my work ;-)

Assuming slight familiarity with the Agda programming language, we motivate the need for
basic concepts of category theory with the aim of discussing adjunctions with
a running example of a detailed construction and proof of a free functor.
Moreover, the article contains a host of `exercises`

whose solutions can be found in the
literate source file. Raw Agda code can be found here.

Since the read time for this article is more than two hours, excluding the interspersed exercises, it may help to occasionally consult a some reference sheets:

Coming from a background in order theory, I love Galois Connections and so
our categorical hammer will not be terminal objects nor limits, but rather adjunctions.
As such, *everything is an adjunction* is an apt slogan for us :-)

-- This file has been extracted from https://alhassy.github.io/PathCat/ -- Type checks with Agda version 2.6.0.

## Discovering Heyting Algebra

We attempt to motivate the structure of a Heyting Algebra by considering ‘inverse problems’.

For example,

- You have a secret number \(x\) and your friend has a secret number \(y\), which you've communicated to each other in person.
- You communicate a ‘message’ to each other by adding onto your secret number.
- Hence, if I receive a number \(z\), then I can
*undo*the addition operation to find the ‘message’ \(m = z - y\).

What if we decided, for security, to change our protocol from using addition to using minimum. That is, we encode our message \(m\) as \(z = x ↓ m\). Since minimum is not invertible, we decide to send our encoded messages with a ‘context’ \(c\) as a pair \((z, c)\). From this pair, a unique number \(m′\) can be extracted, which is not necessarily the original \(m\). Read on, and perhaps you'll figure out which messages can be communicated 😉

This exploration demonstrates that relative pseudo-complements

- Are admitted by the usual naturals precisely when infinity is considered a number;
- Are
*exactly*implication for the Booleans; *Internalises*implication for sets;- Yield
*the largest complementary subgraph*when considering subgraphs.

In some sense, the pseudo-complement is the “best approximate inverse” to forming meets, minima, intersections.

Along the way we develop a number of the theorems describing the relationships between different structural components of Heyting Algebras; most notably the internalisation of much of its own structure.

The article aims to be self-contained, however it may be helpful to look at this lattice cheat sheet (•̀ᴗ•́)و