View all
Type Theory as a Workbench Efficient and Effective Provisioning of Virtual Machines for Artefact Evaluation Follow the Trail! Visualising Bi-Directional Type-Checking as Network Communication. Being Positively Negative. Wiring Circuits is as easy as 0-1-Omega, or is it... Types as Interpreters for HDLs to Graphs. Thoughts on API Design for Dependently-Typed Languages Formalising the (Sub-)Structural Aspects of SystemVerilog Faking Linear Variable Usage Synthesised or Checked? A Framework for Resource Dependent EDSLs in a Dependently Typed Language Defining Intrinsically Typed Data Structures Programming with Holes Building Resource-Dependent EDSLs in a Dependently-Typed Language A Framework for Resource Dependent EDSLs in a Dependently Typed Language The Last Step Decidably Uninformative Mutual Avoidance Well-Typed Expressions lead to Well-Typed Well-Scoped Programs Hutton's Razor(s) On Interfaces and Dependent Types LightClick---A Linear Typed Orchestration Language for System-On-A-Chip Designs A Typing Discipline for Hardware Interfaces. A Typing Discipline for Hardware Interfaces. Value-Dependent Session Design in a Dependently-Typed Language. Computing Types with Idris & Linking Specifications with Implementations. Representing Interfaces when you have no Interfaces. Handling Side-Effects using Resource Dependent Algebraic Effects Revisiting Type-Driven Design of Communicating Systems Type-Driven Development of SoC Architectures. Type-Driven Development of SoC Architectures. A Short Note on Collecting Dependently Typed Values Type-Systems for Describing System-on-a-Chip Architectures. TyDe Denied A Type-System for describing System-on-a-Chip Architectures. A Type-System for describing the Structural Topology of System-on-a-Chip Architectures. Designing Hardware using Session Types and Dependent Types---A First Look Type-Driven Development of Communicating Systems using Idris ICFP Rejection FP Dag 17-Type-Driven Design of Communicating Systems using Idris Off The Beaten Track SPLS-Type-Driven Design of Communicating Systems using Idris Effectful Channel Management Dependent Types and Goal-Oriented DSMLs Tips for using Effects in Idris Dependent Lists Embedded Domain Specific Type Systems for Declarative EDSls Types and Abstract Interpretation An Effectful Logger: Part One
View all
Follow the Trail! Visualising Bi-Directional Type-Checking as Network Communication. Being Positively Negative. Wiring Circuits is as easy as 0-1-Omega, or is it... Types as Interpreters for HDLs to Graphs. Thoughts on API Design for Dependently-Typed Languages Formalising the (Sub-)Structural Aspects of SystemVerilog Faking Linear Variable Usage Synthesised or Checked? A Framework for Resource Dependent EDSLs in a Dependently Typed Language Defining Intrinsically Typed Data Structures Programming with Holes Building Resource-Dependent EDSLs in a Dependently-Typed Language A Framework for Resource Dependent EDSLs in a Dependently Typed Language The Last Step Decidably Uninformative Mutual Avoidance Well-Typed Expressions lead to Well-Typed Well-Scoped Programs Hutton's Razor(s) On Interfaces and Dependent Types LightClick---A Linear Typed Orchestration Language for System-On-A-Chip Designs A Typing Discipline for Hardware Interfaces. A Typing Discipline for Hardware Interfaces. Value-Dependent Session Design in a Dependently-Typed Language. Computing Types with Idris & Linking Specifications with Implementations. Representing Interfaces when you have no Interfaces. Handling Side-Effects using Resource Dependent Algebraic Effects Revisiting Type-Driven Design of Communicating Systems Type-Driven Development of SoC Architectures. Type-Driven Development of SoC Architectures. A Short Note on Collecting Dependently Typed Values Type-Systems for Describing System-on-a-Chip Architectures. A Type-System for describing System-on-a-Chip Architectures. A Type-System for describing the Structural Topology of System-on-a-Chip Architectures.