Software Foundations Textbook Solution
There are some unsolved problems like 'informal proof'.
If you have any questions or find problem in solution, please tell me via issue.
IMPORTANT: This repository is written based on Coq8.4pl6.
You can download Coq8.4pl6 in this link.
- Table Of Contents
- About Software Foundations
- Table Of Solutions
- Whole Solutions
- Author Of This Solutions
Software Foundations is the textbook for Software Foundations course in University of Pennsylvania (Pennsylvania, US) and Programming Language course in Seoul National University (Seoul, Korea) and ... (Give me additional info about).
You can download the latest version of the book in this link.
BUT Be careful, This repository based on version 3.2, not the latest. (I will update in near days.)
This book deals with not only automatic proof, but also mathematical formalization of softwares using Coq language. For more detail information, please check the preface of book
Status columns in next tables have one of the following values.
- Nothing : There is nothing to solve in the file.
- Solved : File is already solved. If you find any error or you have proposal, please report it using issue
- Unsolved : File is not solved yet.
- Unchecked : Not checked whether there is problem or not, yet.
| Section Title | Coq File | HTML File | Status | Updated at |
|---|---|---|---|---|
| Preface | Preface.v | Preface.html | Nothing | 2016/06/10 |
| Basics | Basics.v | Basics.html | Solved | 2016/06/10 |
| Induction | Induction.v | Induction.html | Solved | 2016/06/10 |
| Lists | Lists.v | Lists.html | Solved | 2016/06/10 |
| Poly | Poly.v | Poly.html | Solved | 2016/06/11 |
| MoreCoq | MoreCoq.v | MoreCoq.html | Solved | 2016/06/11 |
| Logic | Logic.v | Logic.html | Solved | 2016/06/11 |
| Prop | Prop.v | Prop.html | Solved | 2016/06/12 |
| MoreLogic | MoreLogic.v | MoreLogic.html | Solved | 2016/06/13 |
| SfLib* | SfLib.v | SfLib.html | Nothing | 2016/06/10 |
| Imp | Imp.v | Imp.html | Solved | 2016/06/13 |
| Equiv | Equiv.v | Equiv.html | Solved | 2016/06/13 |
| Hoare | Hoare.v | Hoare.html | Solved | 2016/06/14 |
| Hoare2 | Hoare2.v | Hoare2.html | Solved | 2016/06/14 |
| Smallstep | Smallstep.v | Smallstep.html | Solved | 2016/06/15 |
| Auto | Auto.v | Auto.html | Nothing | 2016/06/10 |
| Types | Types.v | Types.html | Solved | 2016/06/15 |
| Stlc | Stlc.v | Stlc.html | Solved | 2016/06/15 |
| StlcProp | StlcProp.v | StlcProp.html | Solved | 2016/06/15 |
| MoreStlc | MoreStlc.v | MoreStlc.html | Solved | 2016/06/18 |
| Typechecking | Typechecking.v | Typechecking.html | Nothing | 2016/06/10 |
| References | References.v | References.html | Solved | 2016/06/20 |
| Sub | Sub.v | Sub.html | Unchecked | 2016/06/10 |
| Records | Records.v | Records.html | Unchecked | 2016/06/10 |
| RecordSub | RecordSub.v | RecordSub.html | Unchecked | 2016/06/10 |
| Postscript | Postscript.v | Postscript.html | Nothing | 2016/06/10 |
* Not in blue arrow sequence, but necessary for this sequence.
| Section Title | Coq File | HTML File | Status | Updated at |
|---|---|---|---|---|
| Rel | Rel.v | Rel.html | Unchecked | 2016/06/10 |
| ProofObjects | ProofObjects.v | ProofObjects.html | Unchecked | 2016/06/10 |
| MoreInd | MoreInd.v | MoreInd.html | Unchecked | 2016/06/10 |
| ImpCEvalFun | ImpCEvalFun.v | ImpCEvalFun.html | Unchecked | 2016/06/10 |
| ImpParser | ImpParser.v | ImpParser.html | Unchecked | 2016/06/10 |
| Extraction | Extraction.v | Extraction.html | Unchecked | 2016/06/10 |
| PE | PE.v | PE.html | Unchecked | 2016/06/10 |
| HoareAsLogic | HoareAsLogic.v | HoareAsLogic.html | Unchecked | 2016/06/10 |
| LibTactics | LibTactics.v | LibTactics.html | Nothing | 2016/06/10 |
| UseTactics | UseTactics.v | UseTactics.html | Unchecked | 2016/06/10 |
| UseAuto | UseAuto.v | UseAuto.html | Unchecked | 2016/06/10 |
| Norm | Norm.v | Norm.html | Unchecked | 2016/06/10 |
Junyoung Clare Jang, Ailrun
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent