Formalizing the semantics of a dual-valued functional language in Coq

Simple item page
dc.contributor.advisorvon Ronne, Jeffery
dc.contributor.authorAlders, Eric
dc.contributor.committeeMemberNiu, Jianwei
dc.contributor.committeeMemberLiu, Tongping
dc.date.accessioned2024-01-26T20:46:04Z
dc.date.available2024-01-26T20:46:04Z
dc.date.issued2015
dc.description.abstractWe provide the formalization, in the Coq proof assistant, of a small dual-valued functional language. Particularly, we explore the semantic properties that are required for reasoning about dual-values within a functional language. We formalize four theorems, in Coq, showing their completeness and soundness, of the small-step semantic rules for our small dual-valued functional language. We also highlight differences between the Coq implementation of our proofs from the original work done in this area by Pottier and Simonet with their Core ML2 language.
dc.description.departmentComputer Science
dc.format.extent76 pages
dc.format.mimetypeapplication/pdf
dc.identifier.isbn9781339309125
dc.identifier.urihttps://hdl.handle.net/20.500.12588/2562
dc.languageen
dc.subjectCoq
dc.subjectFormal Proofs
dc.subjectInformation Flow
dc.subjectProgramming Languages
dc.subject.classificationComputer science
dc.subject.lcshFunctional programming languages
dc.subject.lcshAutomatic theorem proving
dc.subject.lcshSemantic computing
dc.titleFormalizing the semantics of a dual-valued functional language in Coq
dc.typeThesis
dc.type.dcmiText
dcterms.accessRightspq_closed
thesis.degree.departmentComputer Science
thesis.degree.grantorUniversity of Texas at San Antonio
thesis.degree.levelMasters
thesis.degree.nameMaster of Science

Files

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
Alders_utsa_1283M_11768.pdf
Size:
501.14 KB
Format:
Adobe Portable Document Format
Download

Collections

Electronic Theses and Dissertations - Open Access