Arthur Charguéraud
Publications
by date
by topic
by venue
Software
OptiTrust
CFML
TLC
PASL
FormalMetaCoq
Teaching
Separation Logic
Coq tutorials
Concours Castor
France-ioi
Misc
The RE command
Home
–
Contact
@InProceedings{harrison-95, author = "John Harrison", title = "Inductive Definitions: Automation and Application", year = "1995", volume = "971", pages = "200--213", editor = "E. Thomas Schubert and Phillip J. Windley and Jim Alves-Foss", publisher = "Springer", series = "LNCS", booktitle = "TPHOLs", }