date: 2021-01-20T17:27:39Z
pdf:PDFVersion: 1.5
pdf:docinfo:title: Lassie: HOL4 Tactics by Example
xmp:CreatorTool: Conference Publishing Consulting
access_permission:can_print_degraded: true
subject: CPP 2021
language: en
dc:format: application/pdf; version=1.5
pdf:docinfo:creator_tool: Conference Publishing Consulting
access_permission:fill_in_form: true
pdf:encrypted: false
dc:title: Lassie: HOL4 Tactics by Example
modified: 2021-01-20T17:27:39Z
cp:subject: CPP 2021
pdf:docinfo:subject: CPP 2021
pdf:docinfo:creator: Heiko Becker, Nathaniel Bos, Ivan Gavran, Eva Darulova, and Rupak Majumdar
PTEX.Fullbanner: This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020) kpathsea version 6.3.2
meta:author: Nathaniel Bos
trapped: False
meta:creation-date: 2020-12-14T09:41:32Z
created: 2020-12-14T09:41:32Z
access_permission:extract_for_accessibility: true
Creation-Date: 2020-12-14T09:41:32Z
Author: Nathaniel Bos
producer: ConfPub - poplws21cppmain-p27-p rev-994e4820c8-48836 p212
pdf:docinfo:producer: ConfPub - poplws21cppmain-p27-p rev-994e4820c8-48836 p212
pdf:unmappedUnicodeCharsPerPage: 0
dc:description: CPP 2021
Keywords: Interactive Theorem Proving;  HOL4;  Semantic Parsing;  Tactic Programming
access_permission:modify_annotations: true
PDFVersion: 1.5
dc:creator: Nathaniel Bos
description: CPP 2021
dcterms:created: 2020-12-14T09:41:32Z
Last-Modified: 2021-01-20T17:27:39Z
dcterms:modified: 2021-01-20T17:27:39Z
title: Lassie: HOL4 Tactics by Example
xmpMM:DocumentID: uuid:d75f759b-1333-4959-9413-3395f7f20a3e
Last-Save-Date: 2021-01-20T17:27:39Z
pdf:docinfo:keywords: Interactive Theorem Proving;  HOL4;  Semantic Parsing;  Tactic Programming
pdf:docinfo:modified: 2021-01-20T17:27:39Z
meta:save-date: 2021-01-20T17:27:39Z
pdf:docinfo:custom:PTEX.Fullbanner: This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020) kpathsea version 6.3.2
pdf:docinfo:custom:PDFVersion: 1.5
Content-Type: application/pdf
X-Parsed-By: org.apache.tika.parser.DefaultParser
creator: Nathaniel Bos
dc:language: en
dc:subject: Interactive Theorem Proving;  HOL4;  Semantic Parsing;  Tactic Programming
access_permission:assemble_document: true
xmpTPg:NPages: 12
pdf:charsPerPage: 3638
access_permission:extract_content: true
access_permission:can_print: true
pdf:docinfo:trapped: False
meta:keyword: Interactive Theorem Proving;  HOL4;  Semantic Parsing;  Tactic Programming
access_permission:can_modify: true
pdf:docinfo:created: 2020-12-14T09:41:32Z