zee.town

Search CTRL + K

zee.town

Search CTRL + K

codememories

oxide>codememory>1

links

always_reading

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

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

Dynamic Programming versus Memoization

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

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

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

testbeda4x2 at main · oxidecomputertestbed

pl

[Haskell&39;23] The Evolution of Effects

A refinement type by any other name weaselhat

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

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

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-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

Enter to select

to navigate

ESC to close

Kell14in author version

#raindrop #links

Metadata

Source URL:: https://www.humprog.org/~stephen/research/papers/kell14in-author-version.pdf
Topics:: #type-systems, #type-theory, #types

Highlights

Connected Pages

Depth

On this page

Metadata
1. Highlights

Pages mentioning this page

No other pages mentions this page