%PDF-1.5
%
1 0 obj
<</Subtype/XML/Type/Metadata/Length 20410>>stream
<?xpacket begin="" id="W5M0MpCehiHzreSzNTczkc9d"?>
<x:xmpmeta xmlns:x="adobe:ns:meta/">
<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#">
<rdf:Description rdf:about="" xmlns:Iptc4xmpCore="http://iptc.org/std/Iptc4xmpCore/1.0/xmlns/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:jav="http://www.niso.org/schemas/jav/1.0/" xmlns:pdf="http://ns.adobe.com/pdf/1.3/" xmlns:pdfaExtension="http://www.aiim.org/pdfa/ns/extension/" xmlns:pdfaField="http://www.aiim.org/pdfa/ns/field#" xmlns:pdfaProperty="http://www.aiim.org/pdfa/ns/property#" xmlns:pdfaSchema="http://www.aiim.org/pdfa/ns/schema#" xmlns:pdfaType="http://www.aiim.org/pdfa/ns/type#" xmlns:pdfaid="http://www.aiim.org/pdfa/ns/id/" xmlns:pdfuaid="http://www.aiim.org/pdfua/ns/id/" xmlns:pdfx="http://ns.adobe.com/pdfx/1.3/" xmlns:pdfxid="http://www.npes.org/pdfx/ns/id/" xmlns:photoshop="http://ns.adobe.com/photoshop/1.0/" xmlns:prism="http://prismstandard.org/namespaces/basic/3.0/" xmlns:stEvt="http://ns.adobe.com/xap/1.0/sType/ResourceEvent#" xmlns:stFnt="http://ns.adobe.com/xap/1.0/sType/Font#" xmlns:xmp="http://ns.adobe.com/xap/1.0/" xmlns:xmpMM="http://ns.adobe.com/xap/1.0/mm/" xmlns:xmpRights="http://ns.adobe.com/xap/1.0/rights/" xmlns:xmpTPg="http://ns.adobe.com/xap/1.0/t/pg/">
<pdfaExtension:schemas>
<rdf:Bag>
<rdf:li rdf:parseType="Resource">
<pdfaSchema:schema>Adobe PDF Schema</pdfaSchema:schema>
<pdfaSchema:prefix>pdf</pdfaSchema:prefix>
<pdfaSchema:namespaceURI>http://ns.adobe.com/pdf/1.3/</pdfaSchema:namespaceURI>
<pdfaSchema:property>
<rdf:Seq>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>Trapped</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>internal</pdfaProperty:category>
<pdfaProperty:description>Indication if the document has been modified to include trapping information</pdfaProperty:description>
</rdf:li>
</rdf:Seq>
</pdfaSchema:property>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaSchema:schema>XMP Media Management Schema</pdfaSchema:schema>
<pdfaSchema:prefix>xmpMM</pdfaSchema:prefix>
<pdfaSchema:namespaceURI>http://ns.adobe.com/xap/1.0/mm/</pdfaSchema:namespaceURI>
<pdfaSchema:property>
<rdf:Seq>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>DocumentID</pdfaProperty:name>
<pdfaProperty:valueType>URI</pdfaProperty:valueType>
<pdfaProperty:category>internal</pdfaProperty:category>
<pdfaProperty:description>UUID based identifier for all versions and renditions of a document</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>InstanceID</pdfaProperty:name>
<pdfaProperty:valueType>URI</pdfaProperty:valueType>
<pdfaProperty:category>internal</pdfaProperty:category>
<pdfaProperty:description>UUID based identifier for specific incarnation of a document</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>VersionID</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>internal</pdfaProperty:category>
<pdfaProperty:description>Document version identifier</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>RenditionClass</pdfaProperty:name>
<pdfaProperty:valueType>RenditionClass</pdfaProperty:valueType>
<pdfaProperty:category>internal</pdfaProperty:category>
<pdfaProperty:description>The manner in which a document is rendered</pdfaProperty:description>
</rdf:li>
</rdf:Seq>
</pdfaSchema:property>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaSchema:schema>IPTC Core Schema</pdfaSchema:schema>
<pdfaSchema:prefix>Iptc4xmpCore</pdfaSchema:prefix>
<pdfaSchema:namespaceURI>http://iptc.org/std/Iptc4xmpCore/1.0/xmlns/</pdfaSchema:namespaceURI>
<pdfaSchema:property>
<rdf:Seq>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>CreatorContactInfo</pdfaProperty:name>
<pdfaProperty:valueType>ContactInfo</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Document creator's contact information</pdfaProperty:description>
</rdf:li>
</rdf:Seq>
</pdfaSchema:property>
<pdfaSchema:valueType>
<rdf:Seq>
<rdf:li rdf:parseType="Resource">
<pdfaType:type>ContactInfo</pdfaType:type>
<pdfaType:namespaceURI>http://iptc.org/std/Iptc4xmpCore/1.0/xmlns/</pdfaType:namespaceURI>
<pdfaType:prefix>Iptc4xmpCore</pdfaType:prefix>
<pdfaType:description>Basic set of information to get in contact with a person</pdfaType:description>
<pdfaType:field>
<rdf:Seq>
<rdf:li rdf:parseType="Resource">
<pdfaField:name>CiAdrCity</pdfaField:name>
<pdfaField:valueType>Text</pdfaField:valueType>
<pdfaField:description>Contact information city</pdfaField:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaField:name>CiAdrCtry</pdfaField:name>
<pdfaField:valueType>Text</pdfaField:valueType>
<pdfaField:description>Contact information country</pdfaField:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaField:name>CiAdrExtadr</pdfaField:name>
<pdfaField:valueType>Text</pdfaField:valueType>
<pdfaField:description>Contact information address</pdfaField:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaField:name>CiAdrPcode</pdfaField:name>
<pdfaField:valueType>Text</pdfaField:valueType>
<pdfaField:description>Contact information local postal code</pdfaField:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaField:name>CiAdrRegion</pdfaField:name>
<pdfaField:valueType>Text</pdfaField:valueType>
<pdfaField:description>Contact information regional information such as state or province</pdfaField:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaField:name>CiEmailWork</pdfaField:name>
<pdfaField:valueType>Text</pdfaField:valueType>
<pdfaField:description>Contact information email address(es)</pdfaField:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaField:name>CiTelWork</pdfaField:name>
<pdfaField:valueType>Text</pdfaField:valueType>
<pdfaField:description>Contact information telephone number(s)</pdfaField:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaField:name>CiUrlWork</pdfaField:name>
<pdfaField:valueType>Text</pdfaField:valueType>
<pdfaField:description>Contact information Web URL(s)</pdfaField:description>
</rdf:li>
</rdf:Seq>
</pdfaType:field>
</rdf:li>
</rdf:Seq>
</pdfaSchema:valueType>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaSchema:schema>PRISM Basic Metadata</pdfaSchema:schema>
<pdfaSchema:prefix>prism</pdfaSchema:prefix>
<pdfaSchema:namespaceURI>http://prismstandard.org/namespaces/basic/3.0/</pdfaSchema:namespaceURI>
<pdfaSchema:property>
<rdf:Seq>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>complianceProfile</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>internal</pdfaProperty:category>
<pdfaProperty:description>PRISM specification compliance profile to which this document adheres</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>publicationName</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Publication name</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>aggregationType</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Publication type</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>bookEdition</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Edition of the book in which the document was published</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>volume</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Publication volume number</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>number</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Publication issue number within a volume</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>pageRange</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Page range for the document within the print version of its publication</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>issn</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>ISSN for the printed publication in which the document was published</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>eIssn</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>ISSN for the electronic publication in which the document was published</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>isbn</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>ISBN for the publication in which the document was published</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>doi</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Digital Object Identifier for the document</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>url</pdfaProperty:name>
<pdfaProperty:valueType>URL</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>URL at which the document can be found</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>byteCount</pdfaProperty:name>
<pdfaProperty:valueType>Integer</pdfaProperty:valueType>
<pdfaProperty:category>internal</pdfaProperty:category>
<pdfaProperty:description>Approximate file size in octets</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>pageCount</pdfaProperty:name>
<pdfaProperty:valueType>Integer</pdfaProperty:valueType>
<pdfaProperty:category>internal</pdfaProperty:category>
<pdfaProperty:description>Number of pages in the print version of the document</pdfaProperty:description>
</rdf:li>
<rdf:li rdf:parseType="Resource">
<pdfaProperty:name>subtitle</pdfaProperty:name>
<pdfaProperty:valueType>Text</pdfaProperty:valueType>
<pdfaProperty:category>external</pdfaProperty:category>
<pdfaProperty:description>Document's subtitle</pdfaProperty:description>
</rdf:li>
</rdf:Seq>
</pdfaSchema:property>
</rdf:li>
</rdf:Bag>
</pdfaExtension:schemas>
<pdf:Producer>pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) kpathsea version 6.3.4; ConfPub - poplws23cppmain-p32-p rev-2b5efd80dd-62534:62535 p182; modified using iText 4.2.0 by 1T3XT</pdf:Producer>
<pdf:Keywords>Verified Compilation, SSA, Gated SSA</pdf:Keywords>
<pdf:PDFVersion>1.5</pdf:PDFVersion>
<dc:format>application/pdf</dc:format>
<dc:title>
<rdf:Alt>
<rdf:li xml:lang="en">Mechanised Semantics for Gated Static Single Assignment</rdf:li>
</rdf:Alt>
</dc:title>
<dc:description>
<rdf:Alt>
<rdf:li xml:lang="en">- Theory of computation -> Operational semantics.Program verification.- Software and its engineering -> Semantics.</rdf:li>
</rdf:Alt>
</dc:description>
<dc:publisher>
<rdf:Bag>
<rdf:li>Association for Computing Machinery</rdf:li>
</rdf:Bag>
</dc:publisher>
<dc:date>
<rdf:Seq>
<rdf:li>2023-01-04T10:43:00Z</rdf:li>
</rdf:Seq>
</dc:date>
<dc:type>
<rdf:Bag>
<rdf:li>Text</rdf:li>
</rdf:Bag>
</dc:type>
<dc:creator>
<rdf:Seq>
<rdf:li>Yann Herklotz</rdf:li>
<rdf:li>Delphine Demange</rdf:li>
<rdf:li>Sandrine Blazy</rdf:li>
</rdf:Seq>
</dc:creator>
<dc:subject>
<rdf:Bag>
<rdf:li>Verified Compilation</rdf:li>
<rdf:li>SSA</rdf:li>
<rdf:li>Gated SSA</rdf:li>
</rdf:Bag>
</dc:subject>
<dc:source>output.tex</dc:source>
<dc:language>
<rdf:Bag>
<rdf:li>en</rdf:li>
</rdf:Bag>
</dc:language>
<dc:identifier>info:doi/10.1145/3573105.3575681</dc:identifier>
<xmp:CreateDate>2023-01-04T10:43:00Z</xmp:CreateDate>
<xmp:ModifyDate>2023-01-17T08:51:43-08:00</xmp:ModifyDate>
<xmp:MetadataDate>2023-01-17T08:51:43-08:00</xmp:MetadataDate>
<xmp:CreatorTool>LaTeX with acmart 2022/04/09 v1.84 Typesetting articles for the Association for Computing Machinery and hyperref 2022-06-13 v7.00r Hypertext links for LaTeX</xmp:CreatorTool>
<xmpMM:DocumentID>uuid:46cef2b1-3390-4a88-9cea-33ef7a3eaef7</xmpMM:DocumentID>
<xmpMM:InstanceID>uuid:590a3395-467f-4d13-be4c-959000ae41dc</xmpMM:InstanceID>
<xmpMM:VersionID>1</xmpMM:VersionID>
<xmpMM:RenditionClass>default</xmpMM:RenditionClass>
<Iptc4xmpCore:CreatorContactInfo rdf:parseType="Resource">
<Iptc4xmpCore:CiAdrCity>London</Iptc4xmpCore:CiAdrCity>
<Iptc4xmpCore:CiAdrCtry>UK</Iptc4xmpCore:CiAdrCtry>
<Iptc4xmpCore:CiEmailWork>yann.herklotz15@imperial.ac.uk</Iptc4xmpCore:CiEmailWork>
</Iptc4xmpCore:CreatorContactInfo>
<prism:complianceProfile>three</prism:complianceProfile>
<prism:publicationName xml:lang="en">Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '23), January 16â•fi17, 2023, Boston, MA, USA</prism:publicationName>
<prism:aggregationType>book</prism:aggregationType>
<prism:volume>1</prism:volume>
<prism:number>1</prism:number>
<prism:isbn>979-8-4007-0026-2</prism:isbn>
<prism:doi>10.1145/3573105.3575681</prism:doi>
<prism:pageCount>15</prism:pageCount>
<xmpTPg:NPages>15</xmpTPg:NPages>
</rdf:Description>
</rdf:RDF>
</x:xmpmeta>
<?xpacket end="w"?>
endstream
endobj
20 0 obj
<</Subtype/Form/Filter/FlateDecode/Matrix[1 0 0 1 0 0]/Type/XObject/FormType 1/Resources<</ProcSet[/PDF/Text]/Font<</F45 42 0 R>>>>/BBox[0 0 612 792]/Length 67>>stream
x3PHW0Pp2@BLL
,
,
B,-Lc=#HBfl\k
|