concept-params
所属分类：Coq
开发工具：Coq
文件大小：0KB
下载次数：0
上传日期：2017-06-19 14:50:12
上 传 者：
sh-1993
说明： STLC中“通用”编程的“概念参数”的Coq形式化，
(Coq formalization of "concept parameters" for "generic" programming in STLC,)
文件列表:
AuxTactics/ (0, 2017-06-19)
AuxTactics/BasicTactics.v (4658, 2017-06-19)
AuxTactics/LibTactics.v (175442, 2017-06-19)
BasicPLDefs/ (0, 2017-06-19)
BasicPLDefs/Identifier.v (7858, 2017-06-19)
BasicPLDefs/Maps.v (8568, 2017-06-19)
BasicPLDefs/Relations.v (7015, 2017-06-19)
BasicPLDefs/Utils.v (771, 2017-06-19)
GenericModuleLib/ (0, 2017-06-19)
GenericModuleLib/SharedDataDefs.v (18890, 2017-06-19)
GenericModuleLib/SimpleModule.v (10334, 2017-06-19)
GenericModuleLib/SinglePassImplModule.v (12113, 2017-06-19)
GenericModuleLib/SinglePassModule.v (7875, 2017-06-19)
LICENSE (1072, 2017-06-19)
Makefile (9305, 2017-06-19)
SetMapLib/ (0, 2017-06-19)
SetMapLib/List2Set.v (19955, 2017-06-19)
SetMapLib/ListPair2FMap.v (38013, 2017-06-19)
_CoqProject (990, 2017-06-19)
configure.sh (100, 2017-06-19)
cpSTLC/ (0, 2017-06-19)
cpSTLC/cpSTLCa.md (5142, 2017-06-19)
cpSTLC/cpSTLCa_Defs.v (71342, 2017-06-19)
cpSTLC/cpSTLCa_Examples.v (15266, 2017-06-19)
cpSTLC/cpSTLCa_Interpreter.v (16860, 2017-06-19)
cpSTLC/cpSTLCa_Props.v (145326, 2017-06-19)
doc-build.sh (118, 2017-06-19)
materials/ (0, 2017-06-19)
materials/belyakova-ftfjp-2017.pdf (417454, 2017-06-19)
# Concept Parameters for Generic Programming
## Concept Parameters in STLC
Coq formalization of "concept parameters" for "generic" programming in STLC.
The first step is to add simple **concepts** and **models** into STLC:
look at `cpSTLCa*` files in [`cpSTLC`](https://github.com/julbinb/concept-params/blob/master/cpSTLC).
Concepts contain function signatures only, models define those functions.
A program in cpSTLCa consists of concepts' and models' definitions and
a term in STLC extended with concept parametrization and model application.
Here is an example of well-typed cpSTLCa program:
```
concept MonoidNat
ident : Nat
op : Nat -> Nat -> Nat
endc
model MNPlus of MonoidNat
ident = 0
op = \x:Nat.\y:Nat. x + y
endm
model MNMult of MonoidNat
ident = 1
op = \x:Nat.\y:Nat. x * y
endm
(* accOrTwice takes MonoidNat concept parameter
and two nats, x and y,
and either accumulates x and y using monoid binary operation
(if x is not equal to identity element)
or accumulates y and y (if x is equal to identity element)
*)
let
accOrTwice = \m#MonoidNat. \x:Nat.\y:Nat. if x == m.ident
then m.op y y
else m.op x y
in
(* sum of 3 5*)
accOrTwice # MNSum 3 5
```
近期下载者：
相关文件：
收藏者：