/software_foundations_solution

Solutions for software foundations textbook

Primary LanguageHTML

Software Foundation Solution

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

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

Table Of Solutions

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.

Solutions Grouped By Road Map

Blue Arrow Of Road Map

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.

Others Of Road Map

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

Whole Solutions

Author Of This Solutions

Junyoung Clare Jang, Ailrun