5 citations · 5 across the 2 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2008★ 5 cited
Cut Elimination for a Logic with Generic Judgments and Induction
Alwen Tiu
This paper presents a cut-elimination proof for the logic , which is an extension of a proof system for encoding generic judgments, the logic $\FOLDNb$ of Miller and Tiu, wit…
cs.LO2007
The Bedwyr system for model checking over syntactic expressions
David Baelde, Andrew Gacek, Dale Miller +2
Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings. This system, written in OCaml, is a direc…