Tags

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

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 the Structural Topology of System-on-a-Chip Architectures.

Formalising the (Sub-)Structural Aspects of SystemVerilog Faking Linear Variable Usage Synthesised or Checked? Defining Intrinsically Typed Data Structures Programming with Holes 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 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. 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. Designing Hardware using Session Types and Dependent Types---A First Look

Wiring Circuits is as easy as 0-1-Omega, or is it... Types as Interpreters for HDLs to Graphs. Formalising the (Sub-)Structural Aspects of SystemVerilog A Framework for Resource Dependent EDSLs in a Dependently Typed Language Building Resource-Dependent EDSLs in a Dependently-Typed Language A Framework for Resource Dependent EDSLs in a Dependently Typed Language 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. 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. 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

Wiring Circuits is as easy as 0-1-Omega, or is it... Types as Interpreters for HDLs to Graphs. A Framework for Resource Dependent EDSLs in a Dependently Typed Language Building Resource-Dependent EDSLs in a Dependently-Typed Language A Framework for Resource Dependent EDSLs in a Dependently Typed Language Value-Dependent Session Design in a Dependently-Typed Language. TyDe Denied 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

Faking Linear Variable Usage Synthesised or Checked? Defining Intrinsically Typed Data Structures Programming with Holes 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

Formalising the (Sub-)Structural Aspects of SystemVerilog LightClick---A Linear Typed Orchestration Language for System-On-A-Chip Designs 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. 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.

Provisioning My First Artifact. Writing a Rebuttal. Hints & Tips A Typing Discipline for Hardware Interfaces. Value-Dependent Session Design in a Dependently-Typed Language. A Short Note on Collecting Dependently Typed Values TyDe Denied ICFP Rejection Off The Beaten Track Dependent Types and Goal-Oriented DSMLs

Formalising the (Sub-)Structural Aspects of SystemVerilog LightClick---A Linear Typed Orchestration Language for System-On-A-Chip Designs 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. 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.

Type-Driven Development of Communicating Systems using Idris FP Dag 17-Type-Driven Design of Communicating Systems using Idris SPLS-Type-Driven Design of Communicating Systems using Idris Effectful Channel Management Tips for using Effects in Idris An Effectful Logger: Part One

Formalising the (Sub-)Structural Aspects of SystemVerilog LightClick---A Linear Typed Orchestration Language for System-On-A-Chip Designs 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 Framework for Resource Dependent EDSLs in a Dependently Typed Language A Framework for Resource Dependent EDSLs in a Dependently Typed Language A Typing Discipline for Hardware Interfaces. A Typing Discipline for Hardware Interfaces.

TyDe Denied ICFP Rejection Off The Beaten Track Dependent Types and Goal-Oriented DSMLs

Type-Driven Development of Communicating Systems using Idris FP Dag 17-Type-Driven Design of Communicating Systems using Idris SPLS-Type-Driven Design of Communicating Systems using Idris Effectful Channel Management

LightClick---A Linear Typed Orchestration Language for System-On-A-Chip Designs Handling Side-Effects using Resource Dependent Algebraic Effects Revisiting Type-Driven Design of Communicating Systems Type-Driven Development of SoC Architectures.

Grading Utilities Some BibLaTeX Tricks to remember Tips for using Effects in Idris An Effectful Logger: Part One

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.

Type-Driven Development of SoC Architectures. Designing Hardware using Session Types and Dependent Types---A First Look SPLS-Type-Driven Design of Communicating Systems using Idris

Provisioning My First Artifact. Writing a Rebuttal. Hints & Tips

Efficient and Effective Provisioning of Virtual Machines for Artefact Evaluation Provisioning My First Artifact.

PIM Update Declaring PIM Bankruptcy again...

Wiring Circuits is as easy as 0-1-Omega, or is it... Types as Interpreters for HDLs to Graphs.

Some BibLaTeX Tricks to remember Colour Blind Aware Semantic Highlighting

Building Resource-Dependent EDSLs in a Dependently-Typed Language A Type-System for describing the Structural Topology of System-on-a-Chip Architectures.

PIM Update Declaring PIM Bankruptcy again...

PIM Update Declaring PIM Bankruptcy again...

Type Theory as a Workbench Efficient and Effective Provisioning of Virtual Machines for Artefact Evaluation

Value-Dependent Session Design in a Dependently-Typed Language. Designing Hardware using Session Types and Dependent Types---A First Look

Wiring Circuits is as easy as 0-1-Omega, or is it... Types as Interpreters for HDLs to Graphs.

My (First) Research Programme TyDe Denied