Interactive Theorem Proving (ITP) is an annual international academic conference on the topic of automated theorem proving, proof assistants and related topics, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. ITP brings together the communities using many systems based on higherorder logic such as ACL2, Coq, Mizar, HOL, Isabelle, Lean, NuPRL, PVS, and Twelf. Individual workshops or meetings devoted to individual systems are usually held concurrently with the conference.
Property  Value 

dbo:abstract 

dbo:wikiPageExternalLink  
dbo:wikiPageID 

dbo:wikiPageLength 

dbo:wikiPageRevisionID 

dbo:wikiPageWikiLink 

dbp:wikiPageUsesTemplate  
dct:subject  
gold:hypernym  
rdf:type  
rdfs:comment 

rdfs:label 

owl:sameAs  
prov:wasDerivedFrom  
foaf:isPrimaryTopicOf  
is dbo:wikiPageDisambiguates of  
is dbo:wikiPageRedirects of  
is dbo:wikiPageWikiLink of 

is foaf:primaryTopic of 