/scientific_papers

📜A repo to store scientific papers

Scientific Papers & Books

Category Theory

  • Seven Sketches in Compositionality: An Invitation to Applied Category Theory
  • Category Theory for Scientists (Old Version)
  • Categories for the Working Mathematician
  • Cofree Traversable Functors
  • Category Theory Using String Diagrams
  • Category Theory
  • Basic Category Theory

Type Theory

  • Homotopy Type Theory: Univalent Foundations of Mathematics
  • Type Systems for Programming Languages
  • A Theory of Type Polymorphism in Programming
  • Generalizing Hindley-Milner Type Inference Algorithms
  • Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
  • Propositions as Types
  • Theorems for Free!
  • Typability and type checking in System F are equivalent and undecidable’
  • Advanced Topics in Types and Programming Languages
  • Type Theory & Functional Programming
  • Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types
  • A Practical Subtyping System For Erlang
  • Wobbly Types: Type Inference For Generalised Algebraic Data Types
  • Proofs and Types
  • In Search of Types
  • Introduction to Univalent Foundations of Mathematics with Agda
  • Bidirectional Typing
  • Program = Proof
  • Formal Topology in Univalent Foundations

Programming Language Theory (general)

  • The Design and Implementation of Typed Scheme
  • A Practical Type Checker for Scheme
  • System F in Agda, for fun and profit
  • From System F to Typed Assembly Language
  • Type checking in the presence of meta-variables

Monads (general)

  • Computational lambda-calculus and monads
  • Monads for functional programming
  • The essence of functional programming
  • Imperative functional programming
  • A Monad for Deterministic Parallelism
  • Burritos for the Hungry Mathematician
  • Toposes of Topological Monoid Actions

Comonads

  • Comonadic Notions of Computation
  • A Real-World Application with a Comonadic User Interface

Free Monads

  • Freer Monads, More Extensible Effects
  • Totality versus Turing-Completeness?

Type Checking

  • Type checking and normalisation
  • Type checking through unification
  • Practical dependent type checking using twin types
  • A Dependently-Typed Linear Ï€-Calculus in Agda
  • Co-Contextual Typing Inference for the Linear Ï€-Calculus in Agda

Dependent Types

  • Dependent Types in Haskell: Theory and Practice
  • Certified Programming with Dependent Types
  • A Tutorial Implementation of a Dependently Typed Lambda Calculus
  • Higher-Order Dynamic Pattern Unification for Dependent Types and Records
  • Dependently Typed Programming in Agda

Linear Types

  • Composable Efficient Array Computations Using Linear Types
  • On the Duality of Streams: How Can Linear Types Help to Solve the Lazy IO Problem?
  • Linear types can change the world!

Fudgets

  • Lazy Functional Components for Graphical User Interfaces

NixOS

  • NixOS: A Purely Functional Linux Distribution
  • The Purely Functional Software Deployment Model

Cubical Type Theory

  • Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom
  • Finiteness in Cubical Type Theory

API design

  • Functional Pearls Ghosts of Departed Proofs

Transient State Electronics

  • Recent development of transient electronics
  • Transient Electronics as Sustainable Systems: From Fundamentals to Applications

Quantum Theory and Proofs

  • An Effect-Theoretic Reconstruction of Quantum Theory
  • MIP* = R
  • International Symposium on Mathematics, Quantum Theory, and Cryptography (2019)

Uncategorized

  • The Implementation of Functional Programming Languages
  • Haskell SpriteKit
  • QED at Large: A Survey of Engineering of Formally Verified Software
  • A Block Design for Introductory Functional Programming in Haskell
  • Efficient Functional Programming using Linear Types: The Array Fragment
  • Exploring Generic Haskell
  • Verified Functional Programming in Agda
  • Retrofitting Linear Types
  • The History of Standard ML
  • A Calculus of Mobile Processes, I & II
  • Efficient Communication and Collection with Compact Normal Form
  • Purely Functional Data Structures
  • How to write a Finanial Contract
  • Composing Contracts: An Adventure in Financial Engineering
  • How to Keep Your Neighbours in Order
  • On the Bright Side of Type Classes: Instance Arguments in Agda