search

mekty2012 / Theories-of-Programming-Languages-Implementation

Implementation of various languages in book Theories of Programming Languages by John C. Reynolds
0 stars 0 forks source link

Refactor all code into Coq #1

Closed mekty2012 closed 4 years ago

mekty2012 commented 4 years ago

The operational semantics visualized here would not reflect well concepts from nondeterminism, and also some features for lambda calculus.

Refactor all code into small step operational semantics given as Inductive Proposition. For details, see programming language foundation in software foundation series.

Also, my goal is to prove that denotational semantics given coincide with operational semantics. Therefore, it may be helpful to have category theory implementation in Coq as library.

mekty2012 commented 4 years ago

Specification

  1. Implement domain theory. Done. Some proof required.
  2. If required, implement category theory related theorems. This repository will be helpful.
  3. ~~Also, adding input&output will makes it harder to create 'good' domain. If required, use coinductive type with follwoing references. http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/bertot_sl2.pdf https://www.labri.fr/perso/casteran/CoqArt/Tsinghua/C7.pdf~~ Done.