This HTML5 document contains 35 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n22doi:10.1007/
dctermshttp://purl.org/dc/terms/
n2https://kar.kent.ac.uk/id/eprint/
wdrshttp://www.w3.org/2007/05/powder-s#
dchttp://purl.org/dc/elements/1.1/
n14http://purl.org/ontology/bibo/status/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n8https://kar.kent.ac.uk/id/subject/
n12https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n5http://eprints.org/ontology/
n17https://kar.kent.ac.uk/id/event/
n9http://www.loc.gov/loc.terms/relators/
bibohttp://purl.org/ontology/bibo/
n18https://kar.kent.ac.uk/id/publication/
n19https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
n6https://kar.kent.ac.uk/id/document/
n13https://kar.kent.ac.uk/id/
n16https://kar.kent.ac.uk/82503/
xsdhhttp://www.w3.org/2001/XMLSchema#
n23https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n10https://kar.kent.ac.uk/id/person/
n4https://kar.kent.ac.uk/id/eprint/82503#

Statements

Subject Item
n2:82503
rdf:type
bibo:BookSection bibo:Article n5:BookSectionEPrint n5:EPrint
rdfs:seeAlso
n16:
owl:sameAs
n22:978-3-030-57761-2_7
n9:EDT
n10:ext-80d06e6727e92fe4a3f0940029f52af3 n10:ext-2986f582695732faef3e1255ff822cb9
n5:hasAccepted
n6:3214502
n5:hasDocument
n6:3214517 n6:3214518 n6:3214502 n6:3214503 n6:3214515 n6:3214516
dc:hasVersion
n6:3214502
dcterms:title
A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang
wdrs:describedby
n12:export_kar_RDFN3.n3 n23:export_kar_RDFN3.n3
dcterms:date
2020-08-17
dcterms:creator
n10:ext-daniel-h@elte.hu n10:ext-4834c5f254471536686f9965adaf5a6b n10:ext-s.j.thompson@kent.ac.uk
bibo:status
n14:peerReviewed n14:published
dcterms:publisher
n19:ext-1c5ddec173ca8cdfba8b274309638579
bibo:abstract
We present a proof-assistant-based formalisation of a subset of Erlang, intended to serve as a base for proving refactorings correct. After discussing how we reused concepts from related work, we show the syntax and semantics of our formal description, including the abstractions involved (e.g. the concept of a closure). We also present essential properties of the formalisation (e.g. determinism) along with the summary of their machine-checked proofs. Finally, we prove expression pattern equivalences which can be interpreted as simple local refactorings.
dcterms:isPartOf
n13:repository n18:ext-03029743
dcterms:subject
n8:QA76.76 n8:QA76
bibo:authorList
n4:authors
bibo:editorList
n4:editors
bibo:presentedAt
n17:ext-6322d7543e5501fb95638c3275d18163
bibo:volume
12222