2 papers
cs.PL2018
Abstract Representation of Binders in OCaml using the Bindlib Library
Rodolphe Lepigre, Christophe Raffalli
The Bindlib library for OCaml provides a set of tools for the manipulation of data structures with variable binding. It is very well suited for the representation of abstract synta…
math.LO2009
Simple proof of the completeness theorem for second order classical and intuitionictic logic by reduction to first-order mono-sorted logic
Karim Nour, Christophe Raffalli
We present a simpler way than usual to deduce the completeness theorem for the second-oder classical logic from the first-order one. We also extend our method to the case of second…