Encoding Proofs in Dedukti: the case of Coq proofs
Author(s) -
Ali Assaf,
Gilles Dowek,
Jean-Pierre Jouannaud,
Jiaxiang Liu
Publication year - 2016
Publication title -
hal (le centre pour la communication scientifique directe)
Language(s) - English
Resource type - Conference proceedings
Subject(s) - mathematical proof , rewriting , proof assistant , computer science , hol , programming language , predicative expression , proof theory , hierarchy , encoding (memory) , calculus (dental) , mathematics , artificial intelligence , philosophy , linguistics , medicine , geometry , dentistry , economics , market economy
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom