Workshop TyDe 2020 – Author Index 
Contents 
Abstracts 
Authors

Allwein, Gerard 
TyDe '20: "Strongly Bounded Termination ..."
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
Thomas Reynolds, William L. Harrison, Rohit Chadha, and Gerard Allwein (University of Missouri, USA; Oak Ridge National Laboratory, USA; U.S. Naval Research Laboratory, USA) Termination checking is a classic static analysis, and, within this focus, there are typebased approaches that formalize termination analysis as type systems (i.e., so that all welltyped programs terminate). But there are situations where a stronger termination property (which we call stronglybounded termination) must be determined and, accordingly, we explore this property via a variant of the simplytyped λcalculus called the boundedtime λcalculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating stronglybounded termination and BTC are described as well. Article Search 

Chadha, Rohit 
TyDe '20: "Strongly Bounded Termination ..."
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
Thomas Reynolds, William L. Harrison, Rohit Chadha, and Gerard Allwein (University of Missouri, USA; Oak Ridge National Laboratory, USA; U.S. Naval Research Laboratory, USA) Termination checking is a classic static analysis, and, within this focus, there are typebased approaches that formalize termination analysis as type systems (i.e., so that all welltyped programs terminate). But there are situations where a stronger termination property (which we call stronglybounded termination) must be determined and, accordingly, we explore this property via a variant of the simplytyped λcalculus called the boundedtime λcalculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating stronglybounded termination and BTC are described as well. Article Search 

Danielsson, Nils Anders 
TyDe '20: "Practical Dependent Type Checking ..."
Practical Dependent Type Checking using Twin Types
Víctor López Juan and Nils Anders Danielsson (Chalmers University of Technology, Sweden; University of Gothenburg, Sweden) People writing proofs or programs in dependently typed languages can omit some function arguments in order to decrease the code size and improve readability. Type checking such a program involves filling in each of these implicit arguments in a typecorrect way. This is typically done using some form of unification. One approach to unification, taken by Agda, involves sometimes starting to unify terms before their types are known to be equal: in some cases one can make progress on unifying the terms, and then use information gleaned in this way to unify the types. This flexibility allows Agda to solve implicit arguments that are not found by several other systems. However, Agda's implementation is buggy: sometimes the solutions chosen are illtyped, which can cause the type checker to crash. With Gundry and McBride's twin variable technique one can also start to unify terms before their types are known to be equal, and furthermore this technique is accompanied by correctness proofs. However, so far this technique has not been tested in practice as part of a full type checker. We have reformulated Gundry and McBride's technique without twin variables, using only twin types, with the aim of making the technique easier to implement in existing type checkers (in particular Agda). We have also introduced a typeagnostic syntactic equality rule that seems to be useful in practice. The reformulated technique has been tested in a type checker for a tiny variant of Agda. This type checker handles at least one example that Coq, Idris, Lean and Matita cannot handle, and does so in time and space comparable to that used by Agda. This suggests that the reformulated technique is usable in practice. Article Search 

Harrison, William L. 
TyDe '20: "Strongly Bounded Termination ..."
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
Thomas Reynolds, William L. Harrison, Rohit Chadha, and Gerard Allwein (University of Missouri, USA; Oak Ridge National Laboratory, USA; U.S. Naval Research Laboratory, USA) Termination checking is a classic static analysis, and, within this focus, there are typebased approaches that formalize termination analysis as type systems (i.e., so that all welltyped programs terminate). But there are situations where a stronger termination property (which we call stronglybounded termination) must be determined and, accordingly, we explore this property via a variant of the simplytyped λcalculus called the boundedtime λcalculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating stronglybounded termination and BTC are described as well. Article Search 

López Juan, Víctor 
TyDe '20: "Practical Dependent Type Checking ..."
Practical Dependent Type Checking using Twin Types
Víctor López Juan and Nils Anders Danielsson (Chalmers University of Technology, Sweden; University of Gothenburg, Sweden) People writing proofs or programs in dependently typed languages can omit some function arguments in order to decrease the code size and improve readability. Type checking such a program involves filling in each of these implicit arguments in a typecorrect way. This is typically done using some form of unification. One approach to unification, taken by Agda, involves sometimes starting to unify terms before their types are known to be equal: in some cases one can make progress on unifying the terms, and then use information gleaned in this way to unify the types. This flexibility allows Agda to solve implicit arguments that are not found by several other systems. However, Agda's implementation is buggy: sometimes the solutions chosen are illtyped, which can cause the type checker to crash. With Gundry and McBride's twin variable technique one can also start to unify terms before their types are known to be equal, and furthermore this technique is accompanied by correctness proofs. However, so far this technique has not been tested in practice as part of a full type checker. We have reformulated Gundry and McBride's technique without twin variables, using only twin types, with the aim of making the technique easier to implement in existing type checkers (in particular Agda). We have also introduced a typeagnostic syntactic equality rule that seems to be useful in practice. The reformulated technique has been tested in a type checker for a tiny variant of Agda. This type checker handles at least one example that Coq, Idris, Lean and Matita cannot handle, and does so in time and space comparable to that used by Agda. This suggests that the reformulated technique is usable in practice. Article Search 

Reynolds, Thomas 
TyDe '20: "Strongly Bounded Termination ..."
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
Thomas Reynolds, William L. Harrison, Rohit Chadha, and Gerard Allwein (University of Missouri, USA; Oak Ridge National Laboratory, USA; U.S. Naval Research Laboratory, USA) Termination checking is a classic static analysis, and, within this focus, there are typebased approaches that formalize termination analysis as type systems (i.e., so that all welltyped programs terminate). But there are situations where a stronger termination property (which we call stronglybounded termination) must be determined and, accordingly, we explore this property via a variant of the simplytyped λcalculus called the boundedtime λcalculus (BTC). This paper presents the BTC and its semantics and metatheory through a Coq formalization. Important examples (e.g., hardware synthesis from functional languages and detection of covert timing channels) motivating stronglybounded termination and BTC are described as well. Article Search 
6 authors
proc time: 1.34