zee.town
Search
CTRL + K
zee.town
Search
CTRL + K
codememories
oxide>codememory>1
links
always_reading
Ahmed
blog-posts-2024-09-10.md at master · frankmcsherry-blog · GitHub
Joe Duffy - A (brief) retrospective on transactional memory
The Bitter Lesson
The Tears of Donald Knuth – Communications of the ACM
What Type Soundness Theorem Do You Really Want to Prove- - SIGPLAN Blog
cmu
Funding Conferences - Office of Graduate and Postdoctoral Affairs - Carnegie Mellon University
cs
5th HLF – Lecture Leslie Lamport
[1hr Talk] Intro to Large Language Models
Aaron Schlesinger&39;s Personal Site
Autolab Autograding for All
Basic memory allocators explained in 10 minutes
Beehive lab notebook Local-first access control
Better Benchmarks Through Graphs - Marc&39;s Blog
blogposts2024-09-10.md at master · frankmcsherryblog
C0 VSCode Language Support - Visual Studio Marketplace
Claiming, auto and otherwise · baby steps
Classic HCI demos
Compiler Development Rust or OCaml
Compiling Pattern Matching
Controlling Queue Delay - ACM Queue
cps in hoot — wingolog
CRDTs go brrr
CS 15-122 Principles of Imperative Computation (Spring 2023)
CTAN Package annotate-equations
div style="max-width 480px;"What Is ChatGPT Doing … and Why Does It Workdiv
Document
Dynamic Programming versus Memoization
Fall2022
Getting Started with Category Theory - Ryan Brewer
Guide for Lab Authors - Autolab Documentation
How fast is bit packing
Interactive Theorem Proving, Guest Lecture - Introduction to Agda, by Jeremy Siek
Introduction to Software Construction
Jepsen Datomic Pro 1.0.7075
Joe Duffy - A (brief) retrospective on transactional memory
Let futures be futures
Maybe Everything Is a Coroutine - Adam Nelson
Metastable failures in the wild
Mix-testing revealing a new class of compiler bugs
More thoughts on claiming · baby steps
My binary vector search is better than your FP32 vectors
New Stack Maps for Wasmtime and Cranelift
newca12awesome-rust-formalized-reasoning An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification
Open Data Structures
Pinned places
Post 1 Datalog, Chain-Forward Computation, and Relational Algebra
Programming ZKPs From Zero to Hero
Quickly identifying a sequence of digits in a string of characters
Readme
References are like jumps
Review Performance Modeling and Design of Computer Systems Queueing Theory in Action
The plan-execute pattern
The sad state of property-based testing libraries
The Solid-State Register Allocator
Tree-Structured Concurrency
Union Types in Rust with Type-Level Lists Shun Kashiwa&39;s Blog
Vector databases (3) Not all indexes are created equal
other
Irssi tricks navigating around Joost&39;s blog
oxide
21 - User Networking API RFD Oxide
63 - Network Architecture RFD Oxide
add bgp message tracking, use real maghemite client by rcgoodfellow · Pull Request 5271 · oxidecomputeromicron
BGP support by rcgoodfellow · Pull Request 3986 · oxidecomputeromicron
External networking by rcgoodfellow · Pull Request 2645 · oxidecomputeromicron
HC30-S4 Security
Home · Dogfood 🐶🦴
omicrondocshow-to-run-simulated.adoc at main · oxidecomputeromicron
omicrondocshow-to-run.adoc at main · oxidecomputeromicron
oxidecomputerdendrite The components needed to drive and manage the Oxide rack switch
RFD Oxide
testbeda4x2 at main · oxidecomputertestbed
pl
21 ordered
[Haskell&39;23] The Evolution of Effects
A refinement type by any other name weaselhat
Aplas11
Compiling Swift generics, Part I - Development Compiler - Swift Forums
Context Sensitive Subtyping
copilot-explorer
Down and Dirty with Semantic Set-theoretic Types (a tutorial) v0.4
Elegant and performant recursion in Rust
Gentle intro to type-level recursion in Rust from zero to HList sculpting
graydon2 Some notes on Rust, mutable aliasing and formal verification
How To Prove It With Lean
Hyperproperties and why they&39;re hard
I&39;m betting on Call-by-Push-Value
Introduction - Counterexamples in Type Systems
journal.stuffwithstuff.com
Kell14in author version
Laurence Tratt Compiled and Interpreted Languages Two Ways of Saying Tomato
Linear Types One-Pager
Oxidizing OCaml Locality
Pattern Types ⊆ Refinement Types - HackMD
Polarized Subtyping CodeArtifact
Proc macro support in rust-analyzer for nightly rustc versions
Programming with Refinement Types
Race Conditions Can Be Useful for Parallelism
Scones, Logical Relations, and Parametricity The n-Category Café
Semantic Subtyping in Luau - Roblox Blog
Semantic Subtyping in Luau
Template for CMU SCS PhD thesis (2006)
The algebra (and calculus!) of algebraic data types
The Better Parts. Douglas Crockford. JS Fest 2018
The borrow checker within · baby steps
The Flix Programming Language
Two little interpreters
Universal domain types
What is logical relations
What is realizability
papers
A blend of intersection types and union types
A bowtie for a beast_ Overloading, eta expansion, and extensible data types
A calculus with recursive types, record concatenation and subtyping
A filter lambda model and the completeness of type assignment
A gentle introduction to semantic subtyping
A logical framework with higher-order rational (circular) terms
A mechanical soundness proof for subtyping over recursive types
A new modular implementation for stateful traits
A new type assignment for λ-terms
A record calculus based on symmetric concatenation
A refinement type by any other name _ weaselhat
A refinement type by any other name
A tale of intersection types
A type assignment for the strongly normalizable lambda-terms
A unified system of type refinements
Adjoint logic
Adjunction models for call-by-push-value with stacks
Algebraic subtyping_ Distinguished dissertation 2017
An extension of the basic functionality theory for the λ-calculus
An ideal model for recursive polymorphic types
An indexed model of recursive types for foundational proof-carrying code
Bidirectional typing
Bisimulation as path type for guarded recursive types
Call-by-push-value - A subsuming paradigm
Call-by-push-value
Call-by-push-value_ Decomposing call-by-value and call-by-name
Coinductive axiomatization of recursive type equality and subtyping
Complete type inference for simple objects
Computation focusing
Contextual refinement types
Counterexamples in type systems - counterexamples in type systems
Covariance and Controvariance_ a fresh look at an old issue (a primer in advanced type systems for learning functional programmers)
Deforestation, program transformation, and cut-elimination
Dependent types in practical programming
Design of the programming language FORSYTHE
Direct foundations for compositional programming
Direct models of the computational lambda-calculus
Disjoint intersection types
Distributing intersection and union types with splits and duality (functional pearl)
Effects and coeffects in call-by-push-value (extended version)
Efficient recursive subtyping
Elaborating intersection and union types
Empowering union and intersection types with integrated subtyping
Explicit refinement types
Extended call-by-push-value - Reasoning about effectful programs and evaluation order
Extensible datasort refinements
Extensible records in a pure calculus of subtyping
F-bounded polymorphism for object-oriented programming
Focusing on refinement typing
Getting F-bounded polymorphism into shape
Gradual type theory
Gradual typing as if types mattered
Gradual typing from theory to practice _ SIGPLAN blog
Hack_ a new programming language for HHVM - engineering at meta
Hybrid intersection types for PCF (extended version)
I'm betting on call-by-push-value · thunderseethe's devlog
Imperative compositional programming
Inheritance is subtyping
Integrating induction and coinduction via closure operators and proof cycles
Intersection and union types - Syntax and semantics
Intersection types and computational effects
Intersection types for a strong call-by-push value - normalisations and solvability
Introduction and elimination, left and right
Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
Iowa type theory commute_ Subtyping, the golden key
Is sound gradual typing dead_
L'arithmetique fonctionnelle du second ordre avec points fixes
Linear logic, monads and the lambda calculus
Linear time addition of fibonacci encodings
Linear type theory for asynchronous session types
LiquidHaskell_ experience with refinement types in the real world
Local type inference
Logical step-indexed logical relations
Machine-checked semantic session typing
Making a type difference_ Subtraction on intersection types as generalized record operations
Maybe not
Mixed Inductive_Coinductive types and strong normalization
Monadic compiler calculation (functional pearl)
Monadic intersection types, relationally
Nested datatypes
Nested session types
On subtyping-relation completeness, with an application to iso-recursive types
On the logical strength of confluence and normalisation for cyclic proofs
On the preciseness of subtyping in session types
On the semantic expressiveness of recursive types
On the semantics of fair parallelism
On the unity of duality
Operations on records
Parametric subtyping for structural parametric polymorphism
Polarised intermediate representation of lambda calculus with sums
Polarity in type theory _ existential type
Polarized higher-order subtyping
Polarized subtyping for sized types
Polarized Subtyping
Polymorphic functions with set-theoretic types_ part 1_ syntax, semantics, and evaluation
Polymorphic functions with set-theoretic types_ Part 2_ Local type inference and type reconstruction
Polymorphic set-theoretic types for functional languages. (Types ensemblistes polymorphes pour les langages fonctionnels)
Positive recursive type assignment
Practical refinement-type checking
Practical subtyping for Curry-Style languages
Preliminary design of the programming language Forsythe
Principal type schemes for an extended type theory
Principal type-schemes for functional programs
Probabilistic call by push value
Programming with intersection types and bounded polymorphism
Programming with union, intersection, and negation types
Recursive subtyping for all
Refined typechecking with Stardust
Refinement kinds - type-safe programming with practical type-level computation
Refinement types and computational duality
Refinement types for haskell
Refinement types for ML
Resolution as intersection subtyping via Modus Ponens
Resumptions, weak bisimilarity and big-step semantics for while with interactive I_O_ An exercise in mixed induction-coinduction
Revisiting iso-recursive subtyping
RustBelt_ securing the foundations of the rust programming language
Search for program structure
Semantic domain_ Focusing is not call-by-push-value
Semantic subtyping for non-strict languages
Semantic subtyping
Semantic subtyping_ Dealing set-theoretically with function, union, intersection, and negation types
Semantics of types for mutable state
Sequent calculi for induction and infinite descent
Set-theoretic types for polymorphic variants
Signals and comonads
Simple type inference for structural polymorphism.
Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types
Sound gradual typing_ only mostly dead
Step-indexed syntactic logical relations for recursive and quantified types
Structural induction and coinduction in a fibrational setting
Structural refinement types
Structural subtyping as parametric polymorphism
Subtyping and intersection types revisited
Subtyping by folding an inductive relation into a coinductive one
Subtyping for session types in the pi-Calculus
Subtyping recursive types
Subtyping union types
Subtyping, declaratively
Sums of uncertainty_ refinements go gradual
Syntactic considerations on recursive types
Syntax and Models of a non-Associative Composition of Programs and Proofs. (Syntaxe et modèles d'une composition non-associative des programmes et des preuves)
Taming the merge operator
The coherence of languages with intersection types
The definition of standard ML (revised)
The duality of classical intersection and union types
The fire triangle_ how to mix substitution, dependent elimination, and effects
The logical basis of evaluation order and pattern-matching
The simple essence of algebraic subtyping_ principal type inference with subtyping made easy (functional pearl)
The situation in logic
Total correctness type refinements for communicating processes
Transfinite step-indexing for termination
Tree automata techniques and applications
Tridirectional typechecking
Type assignment for intersections and unions in call-by-value languages
Type refinements in an open world (extended abstract)
Type systems
Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types
Type-checking unsoundness - standardize treatment of such issues among TypeScript - Issue 9825
Types and programming languages
Types are not sets
Types, abstraction and parametric polymorphism
TypeScript playground - soundness
TypeScript_ Documentation - type compatibility
Union types with disjoint switches
Well-founded recursion with copatterns and sized types
Wellfounded recursion with copatterns_ A unified approach to termination and productivity
What type soundness theorem do you really want to prove_
Will deflation lead to depletion_ On non-monotone fixed point inductions
Research and Reading
Thesis Proposal - Polarized Subtyping
zee.town
How To Prove It With Lean
#raindrop
#links
Metadata
Source URL::
https://djvelleman.github.io/HTPIwL/
Topics::
#how
to prove it,
#lean
,
#proofs
Highlights