Algebra03 同态与同构
Published:
介绍群同态、核、同构、第一同构定理与对应定理。
Posts by Tags
Algebra
Algebra02 子群和商群
Published:
介绍子群、陪集、商群、正规子群及同余关系。
Algebra01 群的定义
Published:
从代数系统出发介绍半群、幺半群、群及其等价定义。
Automata
Automata07 TS
Published:
介绍 Transition System、等价关系、积系统及 LTL 时序逻辑。
Automata06 Complexity
Published:
介绍可判定性、递归语言、P/NP/PSPACE/EXP 及复杂度规约。
Automata05 TM
Published:
介绍图灵机、递归可枚举语言、机器变体与语言闭包性质。
Automata04 PDA
Published:
介绍下推自动机、接受方式、确定性及其与 CFG 的等价性。
Automata03 CFL
Published:
介绍上下文无关文法、推导、二义性及 Chomsky 范式。
Automata02 RE
Published:
介绍正则表达式、正则语言的性质及与有限自动机的等价性。
Automata01 FSM
Published:
介绍 DFA、NFA、ε-NFA 的定义、等价性与 DFA 最小化。
CSAPP
CSAPP实验06 : shlab
Published:
本文尚未展开 shlab 实验内容。
CSAPP实验05: cachelab
Published:
本文尚未展开 cachelab 实验内容。
CSAPP实验04: archlab
Published:
本文尚未展开 archlab 实验内容。
CSAPP实验03 : attacklab
Published:
本文尚未展开 attacklab 实验内容。
CSAPP实验02 : bomblab
Published:
本文尚未展开 bomblab 实验内容。
CSAPP实验01 : datalab
Published:
记录 CSAPP Data Lab 中整数与浮点位级运算题的解法。
Compiler
Compiler04 语法制导翻译
Published:
介绍语法制导定义、继承属性、综合属性与语义动作。
cmm Compiler Design
Published:
记录 Cmm 编译器的解析、AST、类型检查、数据流分析与优化设计。
Compiler03 语法分析
Published:
介绍上下文无关文法、语法树、LL/LR 分析与错误恢复。
Compiler02 词法分析
Published:
介绍词法分析、正则表达式、DFA/NFA 及词法分析器构造。
DFA到等价正则表达式的转化
Published:
通过自动机状态方程和 Arden 定理，将 DFA 转换为等价正则表达式。
Compiler01 Introduction
Published:
介绍编译器流程、前后端结构及词法分析到代码生成的主要阶段。
Concurrency
Concurrency04 Promising
Published:
介绍 Promising Semantics 通过 promises 约束内存行为并避免 OOTA。
Concurrency02 Operational
Published:
用操作语义描述并发系统中的 CPU、内存及 CAS、FAA 等操作。
Concurrency01 HMM
Published:
介绍弱内存模型、happens-before 关系与 Out-of-Thin-Air 行为。
Memory Models
Published:
介绍顺序一致性、TSO 及写缓冲导致的内存可见性问题。
Cpp
Cpp Lambda Quirks
Published:
通过实例解释 C++ Lambda 捕获、静态变量与可变闭包的行为。
Cryptography
密码学07 OWF&HC
Published:
介绍单向函数、硬核谓词及其构造伪随机生成器的关系。
密码学06 HASH
Published:
介绍密码学哈希的抗碰撞性质、Merkle-Damgård 构造及 MAC 应用。
密码学05 MAC
Published:
介绍消息认证码、不可伪造性定义及定长和任意长 MAC 构造。
密码学04 PRG&PRF
Published:
介绍伪随机生成器和伪随机函数，以及它们在多次加密中的应用。
密码学03 Computational
Published:
介绍计算安全、可忽略函数、PPT 对手与私钥加密安全游戏。
密码学02 Perfect
Published:
介绍完美保密、一次一密及其概率定义、证明与局限。
密码学01 Intro
Published:
介绍密码学的安全目标、攻击模型、经典密码与可证明安全。
DLCO
Ubuntu下的数电实验环境配置
Published:
记录 Ubuntu 下安装 Quartus、ModelSim 及 USB-Blaster 的实验环境配置。
Database
DB04 Storage
Published:
介绍数据库的文件、页、块、元组存储及有序数据组织。
DB03 SQL
Published:
介绍 SQL 查询、视图、事务、约束及编程语言与数据库交互。
DB02 Relational
Published:
介绍关系模型、主键与外键，以及基本关系代数操作。
DB01 Intro
Published:
介绍数据库、数据模型、DBMS 分层及存储、查询和事务管理。
CMU-DB Lab
Published:
记录 CMU 数据库 Lab0 Trie 的实现经验与 C++ 指针用法。
Eureka Moments
Jane Street 挂经
Published:
记录 Jane Street 技术面试、onsite 面试题与未获录用的经历。
如何投稿一篇论文
Published:
记录首次投稿论文前后的科研经历、幻灭与反思。
我是如何成为TA的
Published:
记录第一次担任助教的经历、工作、同事及对本科教育的思考。
Futamura Projections
Published:
介绍 Futamura 投影，以及特殊化器、编译器和元编译器的关系。
浅谈Verilog中的X
Published:
讨论 Verilog 中 X 的仿真、综合、验证语义及其精度问题。
A subtle bug in a static analysis framework
Published:
通过常量传播反例分析静态分析框架中的非单调性及其影响。
大三下荒唐实录
Published:
记录大三下的课程、科研、生活及保研经历。
大三上昏睡日志
Published:
记录大三上学期的校园生活、课程体验、工程尝试与日常感想。
大二下摸鱼记录
Published:
记录大二下的校园生活、课程体验及对多门课程的评价。
大二上躺平经验
Published:
记录大二上课程体验、密码学与系统实验，以及留校生活。
大一下存活纪实
Published:
记录大一下的校园生活、课程体验与学习摸鱼经验。
大一上存活经验
Published:
记录大一上校园生活、课程体验与期末复习经验。
半音阶口琴谱合辑
Published:
本文尚未展开半音阶口琴谱内容。
几个关于集合的有趣证明
Published:
用康托尔定理和并集公理证明若干集合构成真类。
有关集合大小的比较
Published:
用双射证明无限集合等势，讨论实数、平面与幂集的大小。
Hello World!
Published:
记录进入大学后的新博客，以及通过写作记录成长的愿望。
Formal Semantics
形式语义05 Semantics
Published:
介绍操作语义及大小步、小步语义，用规则描述程序执行。
形式语义04 Types
Published:
介绍类型系统、类型安全及 STLC 的 Progress 与 Preservation 定理。
形式语义03 Lambda
Published:
系统介绍 Lambda 演算的替换、规约、合流性与递归编码。
形式语义02 Math
Published:
用集合、函数与积和类型的形式化定义说明程序状态和类型构造。
形式语义01 Intro
Published:
介绍形式语义课程动机、程序性质证明及 Coq 形式化验证。
Game Theory
博弈论02 零和游戏
Published:
介绍零和博弈的 min-max 定理、混合策略均衡与线性规划求解。
博弈论01 策略游戏
Published:
介绍纯策略与混合策略博弈、纳什均衡及其求解方法。
Graph Theory
图论04 平面图与可平面图
Published:
介绍平面图、欧拉公式、Kuratowski 定理及极大可平面图的三连通性。
图论03 染色
Published:
讨论点染色、边染色、色多项式、Brooks 定理与平面图染色。
图论01 基本概念&定义
Published:
介绍图的基本类型、邻接、同构、子图、度数和距离等概念。
图论02 匹配
Published:
本文尚未展开图论匹配内容。
ICS
PA4 附加关卡
Published:
记录 PA4 中虚拟内存、进程、中断与加载器 bug 的实现思考。
PA3 附加关卡
Published:
记录 PA3 中栈、异常、ELF 加载、文件系统与库函数实现中的问题。
PA2 附加关卡
Published:
记录 PA2 中声卡、调试追踪、差分测试与 NEMU 实现经验。
PA1 附加关卡
Published:
记录 PA1 中表达式求值、断点和程序测试等基础实验思考。
ICS Intro
信息与计算科学导论03
Published:
介绍集合势、康托定理、不可数性与 Cantor-Bernstein 定理。
信息与计算科学导论02
Published:
讲解递归方程的特征方程、生成函数、算子与主定理。
信息与计算科学导论01
Published:
介绍集合论基础、关系、传递闭包、等价类与函数。
JVM
JVM exception handlers
Published:
分析 JVM 异常处理器顺序及 Java 静态分析中的方法内异常传播。
Linguistics
Linguistics02 Phonetics
Published:
介绍 IPA、辅音和元音，以及发声部位和发声方式。
Linguistics01 Intro
Published:
介绍语言学的研究对象及语音、音系、形态、句法等分支。
Mathematical Logic
数理逻辑03 一阶逻辑
Published:
从命题逻辑扩展到一阶逻辑，介绍项、公式、量词、解释与赋值。
数理逻辑02 推演系统
Published:
介绍 Gentzen 与 Hilbert 推演系统，以及正确性、完备性和一致性。
数理逻辑01 命题逻辑
Published:
介绍命题逻辑的语法、语义、可满足性及 Semantic Tableaux 判定方法。
Network
Network06 Wireless
Published:
介绍无线局域网、隐藏终端、CDMA、802.11、CSMA/CA 与 RTS/CTS。
Network05 Link
Published:
介绍链路层、校验码、共享介质协议、ARP、交换机与 VLAN。
Network04 Network
Published:
介绍网络层、SDN、路由器、IP 编址、NAT 与路由算法。
Network03 Transport
Published:
介绍 UDP、TCP、Socket、可靠传输及 ARQ 协议的基本机制。
Network02 Application
Published:
介绍网络应用、Socket、HTTP、DNS、P2P 与 CDN 等应用层主题。
Network01 Intro
Published:
从分层、交换与接入方式介绍计算机网络和互联网基础。
Numerical Method
计算方法07 电阻网络
Published:
用拉普拉斯矩阵分析电阻网络、电势分布、等效电阻与能量。
计算方法06 FFT
Published:
据助教说不考这么麻烦的计算，我就摸了
计算方法05 图的代数性质
Published:
感觉这部分穿插的有些怪
计算方法04 图的随机游走
Published:
Markov Chain 的本质是概率状态机，这么想就很简单了
计算方法03 线性方程组求解
Published:
这一节主要是玩矩阵，为了偷懒只讨论实线性空间
计算方法02 插值与函数逼近
Published:
心态崩了，这个 latex 公式支持也太迷幻了。
计算方法01 函数求根
Published:
严格写就太累了，这个就当是随手的笔记得了。大概看看原理，不求甚解。
Operating System
操作系统05 调度
Published:
介绍单核与多核任务调度策略、评价指标及公平性问题。
操作系统04 进程与线程
Published:
介绍进程、线程、用户态线程、内核线程与纤程的概念。
操作系统03 内存管理
Published:
介绍虚拟内存、换页、Buddy System、freelist 与 SLAB 分配。
操作系统02 并发
Published:
介绍并发 bug、互斥锁、条件变量、信号量及 RCU 等同步机制。
操作系统01 导引
Published:
从程序、抽象、资源管理与系统调用角度介绍操作系统。
操作系统 Lab3 uproc
Published:
记录用户进程实验中的地址空间、fork、进程管理与内核栈问题。
操作系统 Lab2 kmt
Published:
记录多核任务、信号量与上下文切换实现中的栈竞争和调试问题。
操作系统 Lab1 pmm
Published:
记录多核物理内存分配器的设计、链表与线段树实现及调试经历。
SAT
Tour de SAT
Published:
介绍 SAT、CNF、Resolution、DPLL 及 SAT 求解器搜索策略。
Static Analysis
SA04 Abstract interpretation
Published:
介绍 Galois connection、soundness 与抽象解释的最优性。
SA03 narrowing & widening
Published:
介绍 Widening 加速格上分析，以及 Narrowing 提升分析精度。
SA02 lattice
Published:
介绍格、偏序、单调函数与不动点在静态分析中的作用。
SA01 Type
Published:
介绍类型作为静态分析、递归类型和约束求解类型检查。
软件分析10 Soundiness
Published:
Soundiness 横空出世
软件分析09 CFL-R&IFDS
Published:
这一节主要讨论针对CFG中的路径的优化
软件分析08 Datalog
Published:
Datalog = Data + Logic，是声明式编程语言(Declarative Programming Language) Prolog的一个子集
软件分析07 Security
Published:
本文尚未展开软件分析安全性内容。
软件分析06 CSA
Published:
CSA=Context Sensitive Analysis 上下文敏感分析
软件分析05 PA
Published:
本文尚未展开软件分析 PA 内容。
软件分析04 CGC
Published:
CGC=Call Graph Construction
软件分析03 DFA
Published:
这里的DFA可不是有限状态自动机哦
软件分析02 IR
Published:
本文尚未展开软件分析 IR 内容。
软件分析01 Intro
Published:
决定要好好开干了，于是有了这个系列的笔记
TAOMP
TAOMP02 Mutex
Published:
形式化讨论互斥锁、活性、公平性以及 Peterson、Filter 和 Bakery 算法。
TAOMP01 Intro
Published:
介绍多处理器并发、共享状态、互斥性、活性与 Amdahl 定律。
TAPL
TAPL09 Recursive Types
Published:
介绍递归类型、等递归与同构递归，以及归纳和余归纳不动点。
TAPL08 Subtyping
Published:
介绍子类型关系、函数变型、引用类型及 coercion semantics。
TAPL07 Exceptions
Published:
介绍异常传播、捕获、携带信息及异常处理的类型规则。
TAPL06 References
Published:
介绍可变引用、副作用、别名、存储位置及引用类型检查。
TAPL05 Extensions
Published:
介绍为简单类型 Lambda 演算添加 Unit、Record、Variant、Exception 等语言构造。
TAPL04 Typed Lambda
Published:
介绍简单类型 Lambda 演算及类型唯一性、Progress 和 Preservation 定理。
TAPL03 Untyped Lambda
Published:
介绍无类型 Lambda 演算、规约策略、代数数据类型与 De Bruijn 表示。
TAPL02 Basics
Published:
介绍 TAPL 中的数学记号、语法、操作语义及基本语言性质。
TAPL01 Intro
Published:
介绍类型系统、静态检查、语言安全与类型推导的基本概念。
XCPC
集训补题合集
Published:
汇总多场训练赛题解，涉及树上 DP、卷积、图论与数论。
ICPC 2021 银川划水记
Published:
记录银川 ICPC 线下赛的旅途、比赛过程与赛后感想。
2020 ICPC 小米邀请赛 部分题解
Published:
记录小米邀请赛多道题目的思路、实现与踩坑。
category1
Blog Post number 1
Published:
Sample blog post demonstrating basic Markdown content and headings.
category2
Blog Post number 1
Published:
Sample blog post demonstrating basic Markdown content and headings.
cool posts
Blog Post number 1
Published:
Sample blog post demonstrating basic Markdown content and headings.
haskell
Haskell Parser Combinator
Published:
用 Haskell 实现 Parser Combinator，介绍 Functor、Monad 与解析组合子。
数学分析
数学分析01 实数完备性的六个定理
Published:
串联推导实数完备性的六个等价定理及其相互关系。
数据结构
数据结构01 搜索树
Published:
本文尚未展开搜索树相关内容。
踩坑
LLHD 踩坑记
Published:
记录 Moore/LLHD 工具链构建中的 Rust、依赖与头文件问题。