Toggle navigation
k1r4 Blog
Home
About
Archive
Archive
「FACTA SUNT POTENTIORA VERBIS」
Show All
50
笔记
38
Coq
36
SF (软件基础)
36
PLF (编程语言基础)
19
LF (逻辑基础)
16
payloads
4
web pentest
4
基础
2
C
2
C++
2
Nmap
2
CTF
1
Footprinting
1
Forwading
1
HTB
1
Pivoting
1
QC (Quickcheck)
1
Tools
1
Tunnelin
1
Web Pentest
1
ffuf
1
information gathering
1
metasploit
1
password attack
1
shells
1
web attack
1
2024
Attacking Common Services
Attacking Common Services
File Transfer Cheatseet
File Transfer Cheatseet
Information Gathering Web
Information Gathering Web
Using Metasploit Framework
Using Metasploit Framework
Password Atack
Password Atack
Pivoting, Tunelling & Forwading
Pivoting, Tunelling & Forwading
Atacking Web Applications with Ffuf
Atacking Web Applications with Ffuf
Shells & Payloads
Shells & Payloads
2023
Infrastructure Based Enumeration
Infrastructure Based Enumeration
Nmap CheatSheet
Nmap CheatSheet
CozyHosting : HTB Writeup
CozyHosting Easy Machine
2020
Data Representation - Floating Point Numbers
「数据表示」浮点数
Data Representation - Integer
「数据表示」整数
My Programming Languages Spectrum
我的编程语言光谱
2019
「SF-QC」2 TypeClasses
Quickcheck - A Tutorial on Typeclasses in Coq
「SF-PLF」19 PE
Programming Language Foundations - Partial Evaluation
「SF-PLF」18 UseAuto
Programming Language Foundations - Theory And Practice Of Automation In Coq Proofs
「SF-PLF」17 UseTactics
Programming Language Foundations - Tactic Library For Coq
「SF-PLF」16 LibTactics
Programming Language Foundations - A Collection of Handy General-Purpose Tactics
「SF-PLF」15 Norm
Programming Language Foundations - Normalization of STLC
「SF-PLF」14 RecordSub
Programming Language Foundations - Subtyping with Records
「SF-PLF」13 References
Programming Language Foundations - Typing Mutable References
「SF-PLF」12 Records
Programming Language Foundations - Adding Records To STLC
「SF-PLF」11. TypeChecking
Programming Language Foundations - A Typechecker for STLC
「SF-PLF」10 Sub
Programming Language Foundations - Subtyping (子类型化)
「SF-PLF」9 MoreStlc
Programming Language Foundations - More on The Simply Typed Lambda-Calculus
「SF-PLF」8 StlcProp
Programming Language Foundations - Properties of STLC
「SF-PLF」7 Stlc
Programming Language Foundations - The Simply Typed Lambda-Calculus
「SF-PLF」6 Types
Programming Language Foundations - Type Systems
「SF-PLF」5 Smallstep
Programming Language Foundations - Small-Step Operational Semantics
「SF-PLF」4 HoareAsLogic
Programming Language Foundations - Hoare Logic as a Logic
「SF-PLF」3 Hoare2
Programming Language Foundations - Hoare Logic, Part II
「SF-PLF」2 Hoare
Programming Language Foundations - Hoare Logic, Part I
「SF-PLF」1 Equiv
Programming Language Foundations - Program Equivalence (程序的等价关系)
「SF-LC」15 Auto
Logical Foundations - Extracting ML From Coq
「SF-LC」15 Extraction
Logical Foundations - Extracting ML From Coq
「SF-LC」14 ImpCEvalFun
Logical Foundations - An Evaluation Function For Imp
「SF-LC」13 ImpParser
Logical Foundations - Lexing And Parsing In Coq
「SF-LC」12 Imp
Logical Foundations - Simple Imperative Programs
「SF-LC」11 Rel
Logical Foundations - Properties of Relations
「SF-LC」10 IndPrinciples
Logical Foundations - Induction Principles
「SF-LC」9 ProofObjects
Logical Foundations - The Curry-Howard Correspondence
「SF-LC」8 Maps
Logical Foundations - Total and Partial Maps
「SF-LC」7 Ind Prop
Logical Foundations - Inductively Defined Propositions (归纳定义命题)
「SF-LC」6 Logic
Logical Foundations - Logic in Coq
「SF-LC」5 Tactics
Logical Foundations - More Basic Tactics
「SF-LC」4 Poly
Logical Foundations - Polymorphism and Higher-Order Functions
「SF-LC」3 List
Logical Foundations - Working with Structured Data
「SF-LC」2 Induction
Logical Foundations - Proof by Induction
「SF-LC」1 Basics
Logical Foundations - Functional Programming in Coq
