5eqn

分类

PLT(11) 题解(12)

/ 注册

全部文章（共4篇）

FStar 官方习题 A First Model of Computational Effects

官网写在前面 F* 目前只在 Emacs 有功能全面的编辑器插件，但可惜本人太菜，只会用 Vim，因此只能在线写码。 State Monad 可以理解为封装后的计算，接受初始状态，返回计算结果和后状态。 let st a = int -> a & int read 是一个计算，不...

F*

2023-01-23

2 323

FStar 官方习题 Length-indexed Lists

可参考官网。内容可以将类型的一些属性作为类型的编号，这样在递归定义类型时就可以将属性直接计算出来。例如，以下是定长数组的定义： type vec (a:Type) : nat -> Type = | Nil : vec a 0 | Cons : #n:nat -> hd:...

F*

2023-01-21

0 359

FStar 官方习题 Case Study: Quicksort

概要这一小节讲述了如何用 F* 实现快排算法，并且证明其确实有排序的功能。铺垫：快排实现递归计算 list 长度： let rec length #a (l:list a) : nat = match l with | [] -> 0 | _ :: tl ->...

F*

2023-01-20

0 413

FStar 官方习题 Lemmas and proofs by induction

FStar 是什么？ F* 是一种面向证明的编程语言，运用大量奇技淫巧实现程序自证明，例如：依值类型，Dependent Type，简而言之就是允许类型依赖于具体的值函数式编程，Functional Programming，函数是一等公民，能像值一样作为参数和返回值元语言，Meta Lang...

F*

2023-01-19

1 361