Skip to main content
8 votes
Accepted

What is a weak function space and what does it have to do with HOAS?

In category theory the adjective “weak” is used when the uniqueness parts of a universal property is removed. For example, a weak product of $A$ and $B$ is an object $P$ with morphisms $p_1 : P \to A$ ...
Andrej Bauer's user avatar
  • 9,104
7 votes
Accepted

How to deal with Binders?

There are already a lot of choices pointed out on Jesper Cockx's blog. Usually, the properties you would like to establish includes Equations of compositions of substitutions. For example, $E[x/A][y/...
Trebor's user avatar
  • 3,927
6 votes

Algorithm for the locally nameless representation used by Lean

I implemented the spartan type theory as an educational tool for people who are interested in implementing their own formal systems. If you look at how the type of expressions ...
Andrej Bauer's user avatar
  • 9,104
6 votes
Accepted

Axiomization of Peano arithmetic in constructive first-order logic

Some references: Essential Incompleteness of Arithmetic Verified by Coq includes a formalization of Peano Arithmetic, but it hasn't been kept up-to-date with recent Coq versions AFAIK, and I include ...
Ana Borges's user avatar
4 votes
Accepted

Is there a way to use higher order abstract syntax with linear types?

Yes. The basic idea is to give a HOAS encoding, and then define an auxiliary judgement which checks that variables are used linearly inside a term. Then your typing judgement has additional premises ...
Neel Krishnaswami's user avatar
2 votes

Algorithm for the locally nameless representation used by Lean

I'm not sure what you mean by algorithm, but it sounds like you want to know how an expression is stored internally in Lean. Let's take your example: ...
Jason Rute's user avatar
  • 8,655

Only top scored, non community-wiki answers of a minimum length are eligible