| Posts |
Date Created |
Categories |
| Follow the Trail! Visualising Bi-Directional Type-Checking as Network Communication. |
June 8, 2022 |
idris,dependent-types,asg,protocols,bidi |
| Being Positively Negative. |
June 2, 2022 |
idris,dependent-types |
| Wiring Circuits is as easy as 0-1-Omega, or is it... |
May 31, 2022 |
idris,dependent-types,border-patrol,tdvcs,hdl,systemverilog |
| Types as Interpreters for HDLs to Graphs. |
May 25, 2022 |
idris,dependent-types,border-patrol,tdvcs,hdl,systemverilog |
| Thoughts on API Design for Dependently-Typed Languages |
November 29, 2021 |
idris,type-systems,dependent-types,typing |
| Formalising the (Sub-)Structural Aspects of SystemVerilog |
March 8, 2021 |
idris,soc,hardware,substructural-type-systems,dependent-types,border-patrol,tdd,plas |
| Faking Linear Variable Usage |
January 25, 2021 |
idris,dependent-types,tdd,musing |
| Synthesised or Checked? |
January 22, 2021 |
idris,dependent-types,tdd,musing |
| A Framework for Resource Dependent EDSLs in a Dependently Typed Language |
November 16, 2020 |
idris,dependent-types,border-patrol,tdvcs,ecoop |
| Defining Intrinsically Typed Data Structures |
August 4, 2020 |
idris,dependent-types,tdd,musing |
| Programming with Holes |
July 9, 2020 |
idris,dependent-types,tdd,musing |
| Building Resource-Dependent EDSLs in a Dependently-Typed Language |
June 19, 2020 |
idris,dependent-types,border-patrol,tdvcs,msp101,talk |
| A Framework for Resource Dependent EDSLs in a Dependently Typed Language |
May 28, 2020 |
idris,dependent-types,border-patrol,tdvcs,ecoop |
| The Last Step |
May 26, 2020 |
idris,dependent-types,tdd,musing |
| Mutual Avoidance |
May 4, 2020 |
idris,dependent-types,tdd,musing |
| Decidably Uninformative |
May 4, 2020 |
idris,dependent-types,tdd,musing |
| Well-Typed Expressions lead to Well-Typed Well-Scoped Programs |
December 6, 2019 |
idris,dependent-types,tdd,musing |
| Hutton's Razor(s) |
December 4, 2019 |
idris,dependent-types,tdd,musing |
| On Interfaces and Dependent Types |
November 20, 2019 |
idris,dependent-types,tdd,musing |
| LightClick---A Linear Typed Orchestration Language for System-On-A-Chip Designs |
November 5, 2019 |
idris,soc,hardware,substructural-type-systems,dependent-types,border-patrol,tdd,systems |
| A Typing Discipline for Hardware Interfaces. |
July 10, 2019 |
idris,dependent-types,border-patrol,ecoop |
| Provisioning My First Artifact. |
April 12, 2019 |
paper,advice,repoducible,artifact |
| Writing a Rebuttal. Hints & Tips |
April 2, 2019 |
paper,advice |
| A Typing Discipline for Hardware Interfaces. |
April 1, 2019 |
idris,dependent-types,border-patrol,paper,ecoop |
| Value-Dependent Session Design in a Dependently-Typed Language. |
March 7, 2019 |
idris,dependent-types,session-types,paper,places,tdvcs,border-patrol |
| Computing Types with Idris \& Linking Specifications with Implementations. |
February 12, 2019 |
idris,dependent-types |
| Representing Interfaces when you have no Interfaces. |
February 9, 2019 |
idris,dependent-types,interfaces |
| Revisiting Type-Driven Design of Communicating Systems |
February 5, 2019 |
idris,soc,hardware,substructural-type-systems,dependent-types,border-patrol,tdd,systems |
| Handling Side-Effects using Resource Dependent Algebraic Effects |
February 5, 2019 |
idris,soc,hardware,substructural-type-systems,dependent-types,border-patrol,tdd,systems |
| Type-Driven Development of SoC Architectures. |
December 11, 2018 |
idris,soc,hardware,substructural-type-systems,dependent-types,border-patrol,tdd,systems |
| Type-Driven Development of SoC Architectures. |
October 17, 2018 |
idris,soc,hardware,substructural-type-systems,dependent-types,border-patrol,tdd,spls |
| A Short Note on Collecting Dependently Typed Values |
August 7, 2018 |
idris,dependent-types,paper |
| Type-Systems for Describing System-on-a-Chip Architectures. |
July 12, 2018 |
idris,soc,hardware,linear-types,dependent-types,border-patrol,tdd,pl-interest |
| TyDe Denied |
July 2, 2018 |
idris,tdvcs,border-patrol,paper,tyde,rejection |
| A Type-System for describing System-on-a-Chip Architectures. |
April 5, 2018 |
idris,soc,hardware,linear-types,dependent-types,border-patrol,tdd,stacs-fp |
| A Type-System for describing the Structural Topology of System-on-a-Chip Architectures. |
February 28, 2018 |
idris,soc,hardware,linear-types,dependent-types,border-patrol,tdd,msp101 |
| Designing Hardware using Session Types and Dependent Types---A First Look |
October 11, 2017 |
idris,session-types,border-patrol,tdd,spls |
| Type-Driven Development of Communicating Systems using Idris |
July 25, 2017 |
idris,effects,sessions,tdvcs |
| ICFP Rejection |
March 28, 2017 |
idris,tdvcs,paper,icfp,rejection |
| FP Dag 17-Type-Driven Design of Communicating Systems using Idris |
January 9, 2017 |
idris,effects,sessions,tdvcs |
| Off The Beaten Track |
November 11, 2016 |
idris,tdvcs,paper,obt,rejection |
| Colour Blind Aware Semantic Highlighting |
November 10, 2016 |
latex,accessibility |
| SPLS-Type-Driven Design of Communicating Systems using Idris |
November 9, 2016 |
idris,effects,sessions,tdvcs,spls |
| Effectful Channel Management |
October 5, 2016 |
idris,effects,sessions,tdvcs |
| An Effectful Logger':' Part One |
August 27, 2015 |
idris,effects,tips |
| Tips for using Effects in Idris |
August 14, 2015 |
idris,effects,tips |
| Dependent Types and Goal-Oriented DSMLs |
July 28, 2015 |
idris,phd,paper,gpce,rejection |
| Working With Idris':' Long Compile Times |
July 5, 2015 |
idris,tricks |
| Dependent Lists |
July 5, 2015 |
idris,adt,tricks |
| Types and Abstract Interpretation |
July 4, 2015 |
idris,formal |
| Embedded Domain Specific Type Systems for Declarative EDSls |
July 4, 2015 |
idris |