The Coq mailing list

[Burak Ekici <ekcburak AT hotmail.com>]

Dear Dr. Hutton,

I've inluded below the details of my PhD dissertation regarding your e-mail.

It theoretically deals with computational (side) effects of (impure) programming languages providing formal logics to model them. Also, it implements related formalism in Coq's Gallina, and does some "equational reasoning" there in the tactic language. This might be outside the scope of JFP; if so, sorry for the inconvenience!

Thanks a lot! 

Best,

Burak.

Dissertation title: Certification of programs with computational effects

Student: Burak Ekici 

Awarding institution: Université Grenoble Alpes

Date of PhD award: 09/12/2015

Advisor/supervisor: Jean-Guillaume Dumas and Dominique Duval

Dissertation URL: https://tel.archives-ouvertes.fr/tel-01250842/

Certifications of programs with computational effects

tel.archives-ouvertes.fr

In this thesis, we aim to formalize the effects of a computation. Indeed, most used programming languages involve different sorts of effects: state change, exceptions ...

Dissertation abstract:

In this thesis, we aim to formalize the effects of a computation. Indeed, most used programming languages involve different sorts of effects: state change, exceptions, input/output, non-determinism, etc. They may bring ease and flexibility to the coding process. However, the problem is to take into account the effects when proving the properties of programs. The major difficulty in such kind of reasoning is the mismatch between the syntax of operations with effects and their interpretation. Typically, a piece of program with arguments in X that returns a value in Y is not interpreted as a function from X to Y, due to the effects. The best-known algebraic approach to the problem interprets programs including effects with the use of monads: the interpretation is a function from X to T (Y) where T is a monad. This approach has been extended to Lawvere theories and algebraic handlers. Another approach called, the decorated logic, provides a sort of equational semantics for reasoning about programs with effects. We specialize the approach of decorated logic to the state and the exceptions effects by defining the decorated logic for states (L_st) and the decorated logic for exceptions (L_exc), respectively. This enables us to prove properties of programs involving such effects. Then, we formalize these logics in Coq and certify the related proofs. These logics are built so as to be sound. In addition, we introduce a relative notion of syntactic completeness of a theory in a given logic with respect to a sublogic. We prove that the decorated theory for the global states as well as two decorated theories for exceptions are syntactically complete relatively to their pure sublogics. These proofs are certified in Coq as applications of our generic frameworks.

---

Gönderen: Graham Hutton <Graham.Hutton AT nottingham.ac.uk> adına coq-club-request AT inria.fr <coq-club-request AT inria.fr>
Gönderildi: 10 Nisan 2017 Pazartesi 14:20
Kime: coq-club AT inria.fr
Konu: [Coq-Club] Journal of Functional Programming - Call for PhD Abstracts

 

Dear all,

If you or one of your students recently completed a PhD in the
area of functional programming, please submit the dissertation
abstract for publication in JFP: simple process, no refereeing,
deadline 30th April 2017.  Please share!

Best wishes,

Graham Hutton


============================================================

CALL FOR PHD ABSTRACTS

Journal of Functional Programming

Deadline: 30th April 2017

http://tinyurl.com/jfp-phd-abstracts

============================================================

PREAMBLE:

Many students complete PhDs in functional programming each
year.  As a service to the community, the Journal of Functional
Programming publishes the abstracts from PhD dissertations
completed during the previous year.

The abstracts are made freely available on the JFP website,
i.e. not behind any paywall.  They do not require any transfer
of copyright, merely a license from the author.  A dissertation
is eligible for inclusion if parts of it have or could have
appeared in JFP, that is, if it is in the general area of
functional programming.  The abstracts are not reviewed.

Please submit dissertation abstracts according to the instructions
below.  We welcome submissions from both the PhD student and PhD
advisor/supervisor although we encourage them to coordinate.

============================================================

SUBMISSION:

Please submit the following information to Graham Hutton
<graham.hutton AT nottingham.ac.uk> by 30th April 2017.

o Dissertation title: (including any subtitle)

o Student: (full name)

o Awarding institution: (full name and country)

o Date of PhD award: (month and year; depending on the
 institution, this may be the date of the viva, corrections
 being approved, graduation ceremony, or otherwise)

o Advisor/supervisor: (full names)

o Dissertation URL: (please provide a permanently accessible
 link to the dissertation if you have one, such as to an
 institutional repository or other public archive; links
 to personal web pages should be considered a last resort)

o Dissertation abstract: (plain text, maximum 1000 words;
 you may use \emph{...} for emphasis, but we prefer no
 other markup or formatting in the abstract, but do get
 in touch if this causes significant problems)

Please do not submit a copy of the dissertation itself, as
this is not required.  JFP reserves the right to decline
to publish abstracts that are not deemed appropriate.

============================================================

PHD ABSTRACT EDITOR:

Graham Hutton
School of Computer Science
University of Nottingham
Nottingham NG8 1BB
United Kingdom

============================================================




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it.

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.