Jifeng Wu's Personal Website

2023-05 Spending Statement

10:30 - TalksLinear Types for Systems VerificationIt is a good idea to embed verification information in type system of a programming language. Verified Program Construction Program verification is ha

2023-04 Spending Statement

2023-03 Spending Statement

NOTE: This is a Paper Reading for Topics in Programming Languages: Type Systems. The original paper can be found here. SummaryYou can check the presentation that I made for this paper in this GitHub r

NOTE: This is a Paper Reading for Topics in Programming Languages: Type Systems. The original paper can be found here. SummaryThis paper presents a clear and organized guide to refinement type systems

NOTE: This is a Paper Reading for Topics in Programming Languages: Type Systems. The original paper can be found here. SummaryThe paper first defines and compares parametric and ad-hoc polymorphism an

Fixed-point Combinators, Tying the Recursive Knot, and Recursive Lambda ExpressionsIn Lambda Calculus, we cannot refer to the Lambda Abstraction itself within a Lambda Abstraction. Similarly, C++ does

2023-02 Spending Statement

SummaryChapter 22 of “Types and Programming Languages” explores the problem of Type Reconstruction (Type Inference) or deriving Types for Unannotated Arguments of Lambda Abstractions. It first introdu