semantics-cubNeapolis24: copied from 23

semantics-cubNeapolis24/INSTALL.md

@@ -0,0 +1,113 @@
+### [To the course page](index)
+
+You need to set up an environment on your computer to solve Coq tasks.
+We recommend two alternatives:
+- Direct installation on your machine with Linux/MacOS (harder to setup, but much more convenient to use);
+- Usage of a provided virtual machine image (easier to setup, but less convenient to use).
+
+Once you finish setting up Coq and necessary libraries, you will also need to setup an editor to be able to use Coq interactively.
+Check the corresponding section below.
+
+# Direct installation on your machine with Linux/MacOS
+
+1. In order to install Coq we will use [``opam`` package manager](https://opam.ocaml.org/).
+   You can find the installation instructions for ``opam`` [here](https://opam.ocaml.org/doc/Install.html).
+   Please note, that as of today ``opam`` **does not support** Windows.
+
+2. Initialize ``opam`` by running the following command.
+
+    ```sh
+    opam init -a
+    ```
+
+3. Create a new [switch](https://opam.ocaml.org/doc/Manual.html#Switches). 
+   Switches allow you to easily change the version of OCaml compiler toolchain used to build coq. 
+   Switch creation process may take few minutes.
+
+    ```sh
+    opam switch create semantics 4.12.0
+    opam switch set semantics
+    eval $(opam env)
+    ```
+
+4. Install Coq. In this course we will use Coq version 8.15.2. 
+   You can tell ``opam`` to fix this version using `opam pin` command 
+   (it means that ``opam`` will not try to install more recent versions, even if they are available).
+   Coq installation may take few minutes. 
+
+
+    ```sh
+    opam remote add coq-released https://coq.inria.fr/opam/released
+    opam pin add coq 8.15.2
+    opam install coq
+    ```
+
+5. Install additional Coq libraries required by this course.
+
+   ```sh
+   opam remote add coq-weakmemory-local -k git https://github.com/weakmemory/local-coq-opam-archive
+   opam install coq-hahn
+   ```
+
+6. Check that your environent is propery set up. 
+   Download the course assignments repository. 
+   In the root folder of course assignments run the ``make`` command. 
+   It should start proof-checking the file ``src/b1.v`` and then fail with the message ``Tactic failure: tauto failed``. 
+
+
+7. For proof editing you may use any of the editors proposed in the corresponding section of this manual below.
+   Make sure you have correctly set up editor of your choice.
+   Try to open file ``src/b1.v`` and proof-check it in the step-by-step mode (see below). 
+   It should be checked successfully up until lemma ``nat_eq_tests_pass``. The latter should fail with the message mentioned above.
+
+# Usage of a provided virtual machine image
+
+You can use the [provided virtual machine](https://drive.google.com/file/d/1mn-CwnQKMyEUSTNnCKTPT82Wf7Z-bpin/view?usp=share_link) with Ubuntu 22.04 OS.
+It already has Coq, required libraries and all the code editors installed.
+
+1. Install [VirtualBox](https://www.virtualbox.org/) (we recommend version 6.1), 
+   and [Oracle VM VirtualBox Extension pack](https://www.virtualbox.org/wiki/Downloads).
+
+2. Import the downloaded `.ova` file following the 
+   [instructions](https://docs.oracle.com/en/virtualization/virtualbox/6.0/user/ovf.html#ovf-import-appliance) 
+   in the official documentation.
+
+3. Run the imported VM. 
+  - In case of the error "RawFile#0 failed to create the raw output file ..." try to disable serial ports
+    (In Virtual Box UI select the VM -> Settings -> Serial Ports -> uncheck "Enable Serial Port").
+
+4. Log in to the OS. 
+  - username: vagrant
+  - password: vagrant
+
+5. Check that VM is propery set up.
+   Download the course assignments repository. 
+   In the root folder of course assignments run the ``make`` command. 
+   It should start proof-checking file ``src/b1.v`` and then fail with the message ``Tactic failure: tauto failed``. 
+
+# Editors for interactive work on Coq proofs
+
+Proofs in Coq are intended to be written interactively. To help with that, there exist IDEs and plugins listed below.
+To check that you setted up an editor from the list correctly, open a `*.v` file from the repo
+and execute command "make a step" in the editor.
+
+- You can use specialized editor for Coq --- [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html).
+  Depending on your system, it may require you to install few packages. 
+  For example, on Ubuntu, you need to install ``pkg-config``, ``libgtk-3-dev``, and ``libgtksourceview-3.0-dev``. 
+  CoqIDE itself can be installed via ``opam``: ``opam install coqide``.
+  * Make a step command: button "->" in the toolbox.
+
+- [VSCode](https://code.visualstudio.com/) + [VSCoq](https://github.com/coq-community/vscoq). 
+  * Make a step command: a key combination ``Alt-Down``.
+
+- [Emacs](https://www.gnu.org/software/emacs/) + [Proof General](https://proofgeneral.github.io/). 
+  * Make a step command: button "> Next" in the toolbox, or `C-c C-n` key combination by default.
+  * Find other hot keys [here](https://proofgeneral.github.io/doc/master/userman/Basic-Script-Management/#Basic-Script-Management) (section §2.6).
+  * In Emacs editor some symbols used in the proofs are absent in the default font. 
+    In the Debian-based distribution this issue can be fixed by installing the package ``ttf-ancient-fonts``.
+
+- [Vim](https://www.vim.org/) + [Coqtail](https://github.com/whonore/Coqtail). 
+  * Make a step command: a sequence ``<leader> c j`` (``<leader>`` equals to ``\`` by default).
+
+
+

semantics-cubNeapolis24/hw.md

@@ -0,0 +1,70 @@
+# Homework assignments
+All homework assignments are provided via [GitHub Classroom](https://classroom.github.com/classrooms).
+The assignments are split between two repositories:
+1. (HW1, HW2, HW3) [Coq introductory problems](https://classroom.github.com/a/PDdEEN9_)
+2. (HW4, ...) [Semantics problems](https://classroom.github.com/a/0MM1mmgs)
+
+| HW       | 1     | 2     | 3     | 4      | 5      | 6      | 7      | 8      | 9      |
+|----------|-------|-------|-------|--------|--------|--------|--------|--------|--------|
+| Deadline | Feb 2 | Feb 2 | Feb 5 | Feb 12 | Feb 15 | Mar 2  | Mar  9 | Mar 16 | Mar 23 |
+| Points   | 2     | 2     | 2     | 2      | 2      | 2      | 2      | 2      | 2      |
+
+All assignments are given as Coq proof script files with `.v` extension.
+You supposed to provide all missing definitions and prove admitted lemmas and theorems.
+It is forbidden to modify provided definitions or lemma statements, 
+however you are free to add your own new definitions or auxiliary lemmas.
+Submitted solutions should not contain `admit` or `Admitted`.
+
+## Building Homework Projects
+Both repositories with homeworks are equipped with a `Makefile` 
+that builds all the source files with the assignments. 
+It is sufficient to run `make` command. 
+
+Besides that, `make` command also creates `_CoqProject`. 
+This file is required by the IDE in order to import the project files properly. 
+Thus you might need to run `make` command before you open the homework files in your IDE.
+
+**Important Note.**
+Some assignments depend on files from previous assignments. 
+For example, file `b2.v` imports `b1.v`.
+In order for this import to work (both in batch and interactive mode)
+you need to first build `b1.v` file. 
+Thus, you should perform the following steps: 
+1. complete `b1.v` assignments, check that everything compiles in interactive mode in your IDE;
+2. run `make` to build `b1.v`;
+3. open `b2.v` in your IDE --- now the import of `b1.v` should work. 
+
+## How to submit solutions
+Each individual assignment should be submitted for review as a separate pull request (to some branch in your fork).
+Pull request names should start with "HWn" where "n" is the number of the corresponding homework assignment.
+E.g., the one about "functional programming in Coq" should start with "HW1", and
+the one about "termination of the Euclid's algorithm"--"HW7".
+The diff of each pull request should contain only the files relevant to the submitted assignment,
+i.e., you may create a new branch for each new assignment and make a pull request from it to the previous one.
+When the pull request is ready for review, add the [instructor](https://github.com/eupp/) as an assignee.
+
+## Description of the homework assignments
+
+### Coq introductory problems
+Clone the [repository](https://classroom.github.com/a/PDdEEN9_) with the problems.
+
+1. (HW1) `b1.v` --- functional programming in Coq: implement dictionary abstract datatype in Coq via partial function and list of pairs.  
+
+2. (HW2) `b2.v` --- tactics essentials: prove basic properties of dictionaries.
+
+3. (HW3) `b3.v` --- tactics practice: prove more properties of dictionaries. 
+
+### Semantics problems
+Clone the [repository](https://classroom.github.com/a/0MM1mmgs) with the problems.
+
+4. (HW4) `Id.v` and `State.v` --- prove properties of identifiers and states.
+
+5. (HW5) `Expr.v` --- prove properties of expression language.
+
+6. (HW6) `Stmt.v` --- prove properties of big step semantics.
+
+7. (HW7) `Euclid.v` --- prove termination of the Euclid's algoritm.  
+
+8. (HW8) `SmallStep.v` --- prove properties of small step semantics.
+
+9. (HW9) `Hoare.v` --- prove soundness of the Hoare logic rules.

semantics-cubNeapolis24/index.md

@@ -0,0 +1,34 @@
+# Semantics of Programming Languages (Neapolis, Spring'23)
+
+- [Instructions for setting up environment](INSTALL)
+- [Homework assignments](hw)
+- [Previous class lecture videos (in Russian)](https://www.youtube.com/watch?v=sEiTqZmqY08&list=PLlb7e2G7aSpTA0aT2M1CvIWof3Osslo7Z)
+
+<!-- Задания для знакомых с Coq: -->
+<!-- 1. Доказать существование отсортированной перестановки списка так, -->
+<!-- чтобы при экстракции получался Mergesort. -->
+<!-- 2. Доказать полноту исчисления резолюций. -->
+
+<!-- Задания для знакомых с Coq и семантиками: -->
+<!-- 1. Реализовать операционную модель x86+FPGA из статьи [Iorga-al:OOPSLA21](https://doi.org/10.1145/3485497). -->
+
+### [Coq files from lectures](https://gist.github.com/anlun/0c45a95f961a47ef2e5b75c38632ab92)
+
+<!-- 1. Introduction to semantics  -->
+
+<!-- ### Grading Schema -->
+<!-- TBA -->
+
+### Recommended Textbooks and Resources
+- Glynn Winskel. The Formal Semantics of Programming Languages;
+- Coq tactics cheatsheets:
+[Link 1](http://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf),
+[Link 2](https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html)
+- [Coq Reference Manual](https://coq.inria.fr/distrib/current/refman/);
+- Classical introductory course to logic via Coq, [Software Foundations. Logical Foundations](https://softwarefoundations.cis.upenn.edu/lf-current/index.html).
+
+### Requirements
+- Basic knowledge of functional programming will be a plus:
+-- algebraic data types, lists, etc.
+- Essential understanding and knowledge of propositional logic is expected:
+-- conjunction, disjunction, logical implication, etc.