ComFreek

As a follow-up to today's discussion of HOAS, here is another example: https://en.wikipedia.org/wiki/Higher-order_abstract_syntax#Use_in_logical_frameworks

That example is based on Twelf, which for the purpose of that example, you can think of MMT. In fact, Twelf can be seen as a predecessor of MMT.

Apparently, there's also this classic paper by Pfenning and Elliott on HOAS. The paper's presentation might be a bit too far away from MMT for it to be easily understandable to you. But Section 2 ("motivating examples") might still be of interest to you: it mentions problems of substitution and variable occurrences, which you usually have if you're representing bound variables as mere "string references". I think you might be able to understand bits even if not all of the syntax. (Neither do I understand their syntax by mere glancing.)

By employing, HOAS we completely forego those problems by using meta-level functions (namely from LF). (Internally, these do work

ComFreek

\documentclass[]{article}

% Make `:` behave as if you typed `\colon`.
% In particular, this allows you to concisely write `t: A` for a typing assertion while still
% getting the correct spacing of `\colon`.
%
% source: <https://chat.stackexchange.com/transcript/message/56900862#56900862>
% author: Skillmon <https://tex.stackexchange.com/users/117050/skillmon>
\begingroup
\lccode`\~=`\:

ComFreek

Automatically save your WeeChat configuration and buffer list every day (24h have 86400000 milliseconds):

/trigger add autosave_config_timer timer 86400000;0;0 ""  "" "/mute /save"
/trigger add autosave_join_timer timer 86400000;0;0 ""  "" "/mute /autojoin --rune"
/trigger add autosave_layout_timer timer 86400000;0;0 ""  "" "/mute /layout store"

Upon an upgrade, restore:

ComFreek

Games by Natomic Studios (I like) + Downloads

• Natomic Studios: group of developers which published games created with Multimedia Fusion in early 2000s; they do have a "Natomic Studios" Facebook page
• The Daily Click: website collecting current and old games that are all done with Multimedia Fusion (?)

Note on running the games

• You might need a cnc232.dll -- a runtime library of Multimedia Fusion. Here's a version of cnc232.dll archived by The Wayback Machine. Put it into the same folder as the .exe of the game that interests you and that needs the library.
• Bananarama has a slow movement of the monkey character on Windows Vista and upwards. The game music is still fine, and it's still playable, prob

ComFreek

From Coq Require Import Init.Logic.

Axiom X: Type.
Axiom a b: X.

Axiom P: X -> Prop.
Axiom Q: P b -> Prop.

(*

ComFreek

POPL 2021: https://app.clowdr.org/conference/popl2021

• Mechanized Logical Relations for Termination-Insensitive Noninterference
• A practical mode system for recursive definitions
• λs: Computable semantics for differentiable programming with higher-order functions and datatypes
• On the Semantic Expressiveness of Recursive Types - very funny lightning talk

ComFreek

% !TeX TS-program = xelatex

\documentclass[]{article}
\usepackage{unicode-math}

\begin{document}

\noindent
% These lines render the same
$Γ ⊢ (M ⊧ φ)$\\

ComFreek

mpm --update ; mpm --update --admin ; mpm --update ; mpm --update --admin ; mpm --update-db ; mpm --update-db --admin

ComFreek

Problem: Despite git fetch --all, git branch --all just shows your local branches.

Cause: Did you clone your repository initially with git clone -b <branch name> <remote>? You can very this by running:

$> git config remote.origin.fetch

+refs/heads/<branch name>:refs/remotes/origin/<branch name>

ComFreek

package com.github.comfreek.finchexample

import java.io.{PrintWriter, StringWriter}

import cats.effect.IO
import com.twitter.finagle.Service
import com.twitter.finagle.http.{Request, Response, Status}
import io.circe.{Encoder, Json}
import io.finch._