About: A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang Goto Sponge NotDistinct Permalink

An Entity of Type : bibo:BookSection, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/BookSectionEPrint http://eprints.org/ontology/EPrint Article Book Section
seeAlso	HTML Summary of #82503 A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang
sameAs	A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang
http://www.loc.gov...erms/relators/EDT	Aleksander Byrski John Hughes
http://eprints.org/ontology/hasAccepted	A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang (PDF)
http://eprints.org/ontology/hasDocument	A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang (PDF) A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang (Other) A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang (Other) A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang (Other) A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang (Other) A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang (Other)
dc:hasVersion	A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang (PDF)
Title	A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang
described by	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2020-08-17
Creator	Péter Bereczky Daniel Horpacsi Simon Thompson
status	peer reviewed published
Publisher	Springer
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.
Is Part Of	Financial Cryptography and Data Security https://kar.kent.ac.uk/id/repository
Subject	QA 76 Software, computer programming, QA76.76 Computer software
list of authors	https://kar.kent.ac.uk/id/eprint/82503#authors
list of editors	https://kar.kent.ac.uk/id/eprint/82503#editors
presented at	International Symposium on Trends in Functional Programming
volume	12222
is topic of	https://www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #82503 A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 13 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software