GitHub - amblafont/unification: Notes (and implementation) of unification with binders

Generic pattern unification implemented in Agda (tested with v2.7.0.1, with standard library v2.1.1).

Contents:

lib.lagda: some general purpose definitions and lemmas
lc.lagda (~450 LoC): pattern unification for λ-calculus
main.lagda (~300 LoC): generic pattern unification
common.lagda (~175 LoC): Agda code shared verbatim between lc.lagda and main.lagda
lcsig.lagda: signature for λ-calculus
systemF.agda (~800 LoC): signature for system F

Name		Name	Last commit message	Last commit date
Latest commit History 236 Commits
.vscode		.vscode
diagrams		diagrams
latex-agda		latex-agda
.gitignore		.gitignore
Common.lagda		Common.lagda
Makefile		Makefile
README.md		README.md
acmart-preload-hook.tex		acmart-preload-hook.tex
agda.sty		agda.sty
bib.bib		bib.bib
common-preamble.tex		common-preamble.tex
core.lyx		core.lyx
draft.lyx		draft.lyx
draft.pdf		draft.pdf
ebutf8.sty		ebutf8.sty
fullshort.sty		fullshort.sty
jfp.cls		jfp.cls
jfp.layout		jfp.layout
jfplike.bst		jfplike.bst
lc.lagda		lc.lagda
lcsig.lagda		lcsig.lagda
lib.lagda		lib.lagda
lics24-response.md		lics24-response.md
lics24-reviews.md		lics24-reviews.md
lncs-long.lyx		lncs-long.lyx
lncs-long.pdf		lncs-long.pdf
lncs.lyx		lncs.lyx
main.lagda		main.lagda
main.lyx		main.lyx
main.ml		main.ml
main.pdf		main.pdf
nominal.lyx		nominal.lyx
nominal.pdf		nominal.pdf
occurcheckind.agda		occurcheckind.agda
pbkB-present.json		pbkB-present.json
pbkBsimp.json		pbkBsimp.json
pbkBsimp2.json		pbkBsimp2.json
popl24-response.md		popl24-response.md
popl24-reviews.md		popl24-reviews.md
popl25-response.txt		popl25-response.txt
popl25-reviews.md		popl25-reviews.md
quiver.sty		quiver.sty
refstyle.cfg		refstyle.cfg
refstyle.sty		refstyle.sty
short.lyx		short.lyx
short.pdf		short.pdf
slides.lyx		slides.lyx
slides.pdf		slides.pdf
splncs04.bst		splncs04.bst
systemF.agda		systemF.agda
unification.agda-lib		unification.agda-lib
unifier-v12.json		unifier-v12.json

Provide feedback