# SoftwareFoundations

**Repository Path**: whst/SoftwareFoundations

## Basic Information

- **Project Name**: SoftwareFoundations
- **Description**: 软件基础
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2018-07-28
- **Last Updated**: 2020-12-19

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Software Foundations

Sat Jul 28 09:56:02 CST 2018

initialised by WHsT

This repository contains my solutions to exercises in *Software Foundations*.

## VOLUME 1: Logical Foundations
- [x] Functional Programming in Coq	(Basics)
- [x] Proof by Induction	(Induction)
- [x] Working with Structured Data	(Lists)
- [x] Polymorphism and Higher-Order Functions	(Poly)
- [x] More Basic Tactics	(Tactics)
- [x] Logic in Coq	(Logic)
- [x] Inductively Defined Propositions	(IndProp)
- [x] Total and Partial Maps	(Maps)
- [x] The Curry-Howard Correspondence	(ProofObjects)
- [x] Induction Principles	(IndPrinciples)
- [x] Properties of Relations	(Rel)
- [ ] Simple Imperative Programs	(Imp)
- [ ] Lexing and Parsing in Coq	(ImpParser)
- [x] An Evaluation Function for Imp	(ImpCEvalFun)
- [x] Extracting ML from Coq	(Extraction)
- [x] More Automation	(Auto)

## VOLUME 2: Programming Language Foundations
- [ ] Program Equivalence	(Equiv)
- [ ] Hoare Logic, Part I	(Hoare)
- [ ] Hoare Logic, Part II	(Hoare2)
- [ ] Hoare Logic as a Logic	(HoareAsLogic)
- [x] Small-step Operational Semantics	(Smallstep)
- [ ] Type Systems	(Types)
- [ ] The Simply Typed Lambda-Calculus	(Stlc)
- [ ] Properties of STLC	(StlcProp)
- [ ] More on the Simply Typed Lambda-Calculus	(MoreStlc)
- [ ] Subtyping	(Sub)
- [ ] A Typechecker for STLC	(Typechecking)
- [ ] Adding Records to STLC	(Records)
- [ ] Typing Mutable References	(References)
- [ ] Subtyping with Records	(RecordSub)
- [ ] Normalization of STLC	(Norm)
- [ ] A Collection of Handy General-Purpose Tactics	(LibTactics)
- [ ] Tactic Library for Coq: A Gentle Introduction	(UseTactics)
- [ ] Theory and Practice of Automation in Coq Proofs	(UseAuto)
- [ ] Partial Evaluation	(PE)

## VOLUME 3: Verified Functional Algorithms
- [ ] Basic Techniques for Permutations and Ordering	(Perm)
- [ ] Insertion Sort	(Sort)
- [ ] Insertion Sort With Multisets	(Multiset)
- [ ] Selection Sort, With Specification and Proof of Correctness	(Selection)
- [ ] Binary Search Trees	(SearchTree)
- [ ] Abstract Data Types	(ADT)
- [ ] Running Coq programs in ML	(Extract)
- [ ] Implementation and Proof of Red-Black Trees	(Redblack)
- [ ] Number Representations and Efficient Lookup Tables	(Trie)
- [ ] Priority Queues	(Priqueue)
- [ ] Binomial Queues	(Binom)
- [ ] Programming with Decision Procedures	(Decide)
- [ ] Graph Coloring	(Color)