Skip to content

Instantly share code, notes, and snippets.

View ComFreek's full-sized avatar
💭
I may be slow to respond.

ComFreek ComFreek

💭
I may be slow to respond.
View GitHub Profile
@ComFreek
ComFreek / Explanation of Higher Order Abstract Syntax in Twelf and MMT.md
Created February 4, 2021 19:02
Explanation of Higher Order Abstract Syntax in Twelf and MMT

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
ComFreek / Make LaTeX colons have the spacing of \colon, e.g. for typing judgements.tex
Last active March 3, 2021 12:27
Make LaTeX colons have the spacing of \colon, e.g. for typing judgements.tex
\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
ComFreek / WeeChat: automatically save your configuration.md
Last active January 21, 2021 13:15
WeeChat: automatically save your configuration.md

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
ComFreek / Nostalgic games from Natomic Studios, Bananarama, BI-NARY, BII-NARY.md
Last active January 16, 2021 12:58
Nostalgic games from Natomic Studios, Bananarama, BI-NARY, BII-NARY

Games by Natomic Studios (I like) + Downloads

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
ComFreek / Rewrite equality in type definitions in Coq.v
Created January 14, 2021 15:11
Rewrite equality in type definitions in Coq
From Coq Require Import Init.Logic.
Axiom X: Type.
Axiom a b: X.
Axiom P: X -> Prop.
Axiom Q: P b -> Prop.
(*
@ComFreek
ComFreek / POPL 2021 Talks I find interesting.md
Last active January 11, 2021 09:56
POPL 2021 Talks I find interesting
@ComFreek
ComFreek / Use Unicode characters in TeX sources (with XeLaTeX) to have more readable TeX sources.tex
Created January 2, 2021 21:54
Use Unicode characters in TeX sources (with XeLaTeX) to have more readable TeX sources
% !TeX TS-program = xelatex
\documentclass[]{article}
\usepackage{unicode-math}
\begin{document}
\noindent
% These lines render the same
$Γ ⊢ (M ⊧ φ)$\\
@ComFreek
ComFreek / Update MikTeX on Windows using CLI.ps1
Created December 27, 2020 11:47
Update MikTeX on Windows using CLI
mpm --update ; mpm --update --admin ; mpm --update ; mpm --update --admin ; mpm --update-db ; mpm --update-db --admin
@ComFreek
ComFreek / Git: fix cannot checkout remote branches at all.md
Last active December 14, 2020 12:08
Fix: Git cannot checkout remote branches

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
ComFreek / graceful-finch-server-endpoints.scala
Last active October 27, 2020 12:19
Make Finch servers more graceful for debugging: requests are logged + exceptions are reported to the HTTP client (instead of empty HTTP 500 response)
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._