TyDe '23: "Semantic Encapsulation using ..."
Semantic Encapsulation using Linking Types
Daniel Patterson, Andrew Wagner, and Amal Ahmed
(Northeastern University, USA)
Interoperability pervades nearly all mainstream language implementations, as most systems leverage subcomponents written in different languages. And yet, such linking can expose a language to foreign behaviors that are internally inexpressible, which poses a serious threat to safety invariants and programmer reasoning. To preserve such invariants, a language may try to add features to limit the reliance on external libraries, but endless extensions can obscure the core abstractions the language was designed to provide.
In this paper, we outline an approach that encapsulates foreign code in a sound way—i.e., without disturbing the invariants promised by types of the core language. First, one introduces novel linking types that characterize the behaviors of foreign libraries that are inexpressible in the core language. To reason about the soundness of linking, one constructs a realizability model that captures the meaning of both core types and linking types as sets of target-language terms. Using this model, one can formally prove when foreign behavior is encapsulated; that is, unobservable to core code. We show one way to discharge such proofs automatically by augmenting the compiler to insert verified encapsulation wrappers around components that use foreign libraries.
Inspired by existing approaches to FFIs, we develop a pair of case studies that extend a pure, functional language: one extension for state, and another for exceptions. The first allows us to implement mutable references via a library, whereas the second allows us to implement try and catch as library functions. Both extensions and the overall system are proven sound using logical relations that use realizability techniques.
@InProceedings{TyDe23p14,
author = {Daniel Patterson and Andrew Wagner and Amal Ahmed},
title = {Semantic Encapsulation using Linking Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {14--28},
doi = {10.1145/3609027.3609405},
year = {2023},
}
Publisher's Version
TyDe '23: "A Dependently Typed Language ..."
A Dependently Typed Language with Dynamic Equality
Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, and Hongwei Xi
(Autodesk, USA; Boston University, USA)
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories. We address this issue by designing a dependently typed language where equality checking is delayed until runtime. What were once static errors can now be presented to programmers as warnings. When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution. We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language. Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage. Finally, we have implemented a prototype of the language.
@InProceedings{TyDe23p44,
author = {Mark Lemay and Qiancheng Fu and William Blair and Cheng Zhang and Hongwei Xi},
title = {A Dependently Typed Language with Dynamic Equality},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {44--57},
doi = {10.1145/3609027.3609407},
year = {2023},
}
Publisher's Version
TyDe '23: "Combining Dependency, Grades, ..."
Combining Dependency, Grades, and Adjoint Logic
Peter Hanukaev and Harley Eades III
(Augusta University, USA)
We propose two new dependent type systems. The first, is a dependent graded/linear type system where a graded dependent type system is connected via modal operators to a linear type system in the style of Linear/Non-linear logic. We then generalize this system to support many graded systems connected by many modal operators through the introduction of modes from Adjoint Logic. Finally, we prove several meta-theoretic properties of these two systems including graded substitution.
@InProceedings{TyDe23p58,
author = {Peter Hanukaev and Harley Eades III},
title = {Combining Dependency, Grades, and Adjoint Logic},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {58--70},
doi = {10.1145/3609027.3609408},
year = {2023},
}
Publisher's Version
TyDe '23: "A Dependently Typed Language ..."
A Dependently Typed Language with Dynamic Equality
Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, and Hongwei Xi
(Autodesk, USA; Boston University, USA)
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories. We address this issue by designing a dependently typed language where equality checking is delayed until runtime. What were once static errors can now be presented to programmers as warnings. When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution. We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language. Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage. Finally, we have implemented a prototype of the language.
@InProceedings{TyDe23p44,
author = {Mark Lemay and Qiancheng Fu and William Blair and Cheng Zhang and Hongwei Xi},
title = {A Dependently Typed Language with Dynamic Equality},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {44--57},
doi = {10.1145/3609027.3609407},
year = {2023},
}
Publisher's Version
TyDe '23: "A Calculus of Inductive Linear ..."
A Calculus of Inductive Linear Constructions
Qiancheng Fu and Hongwei Xi
(Boston University, USA)
In this paper, we present a novel calculus of inductive linear constructions (CILC), combining linear types and dependent types. Our type theory addresses a looming issue in the research on linear dependent types: the lack of a general mechanism for defining sound linear inductive types. CILC allows one to encode in a straightforward manner the linear connectives that must be baked into the core of other systems. This greatly lowers the difficulty of encoding various data structures and makes writing non-trivial programs humanly feasible. We study the standard meta theory of our calculus, showing that it is sound in the usual sense. Through a heap-based operational semantics, we show that CILC safely manipulates resources and runs memory clean. We have formalized and proven correct most of the reported results in the Coq Proof Assistant.
@InProceedings{TyDe23p1,
author = {Qiancheng Fu and Hongwei Xi},
title = {A Calculus of Inductive Linear Constructions},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3609027.3609404},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
TyDe '23: "Combining Dependency, Grades, ..."
Combining Dependency, Grades, and Adjoint Logic
Peter Hanukaev and Harley Eades III
(Augusta University, USA)
We propose two new dependent type systems. The first, is a dependent graded/linear type system where a graded dependent type system is connected via modal operators to a linear type system in the style of Linear/Non-linear logic. We then generalize this system to support many graded systems connected by many modal operators through the introduction of modes from Adjoint Logic. Finally, we prove several meta-theoretic properties of these two systems including graded substitution.
@InProceedings{TyDe23p58,
author = {Peter Hanukaev and Harley Eades III},
title = {Combining Dependency, Grades, and Adjoint Logic},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {58--70},
doi = {10.1145/3609027.3609408},
year = {2023},
}
Publisher's Version
TyDe '23: "A Dependently Typed Language ..."
A Dependently Typed Language with Dynamic Equality
Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, and Hongwei Xi
(Autodesk, USA; Boston University, USA)
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories. We address this issue by designing a dependently typed language where equality checking is delayed until runtime. What were once static errors can now be presented to programmers as warnings. When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution. We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language. Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage. Finally, we have implemented a prototype of the language.
@InProceedings{TyDe23p44,
author = {Mark Lemay and Qiancheng Fu and William Blair and Cheng Zhang and Hongwei Xi},
title = {A Dependently Typed Language with Dynamic Equality},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {44--57},
doi = {10.1145/3609027.3609407},
year = {2023},
}
Publisher's Version
TyDe '23: "Infix-Extensible Record Types ..."
Infix-Extensible Record Types for Tabular Data
Adam Paszke and Ningning Xie
(Google DeepMind, Germany; Google DeepMind, Canada)
We present a novel row-polymorphic record calculus, supporting a unique combination of features: scoped labels, first-class labels and rows, and record concatenation. Our work is motivated by the similarity of record types and data table (or data frame) schemas, commonly used in data processing tasks. After presenting our record calculus, we demonstrate its applicability to data frame manipulation by showing that it can be used to successfully assign types to the functions listed in the Brown Benchmark for Tabular Types. Our typing discipline is remarkably lightweight, compared to calculi that require reasoning about type-level constraints when manipulating record types, making it a viable candidate for practical use.
@InProceedings{TyDe23p29,
author = {Adam Paszke and Ningning Xie},
title = {Infix-Extensible Record Types for Tabular Data},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {29--43},
doi = {10.1145/3609027.3609406},
year = {2023},
}
Publisher's Version
TyDe '23: "Semantic Encapsulation using ..."
Semantic Encapsulation using Linking Types
Daniel Patterson, Andrew Wagner, and Amal Ahmed
(Northeastern University, USA)
Interoperability pervades nearly all mainstream language implementations, as most systems leverage subcomponents written in different languages. And yet, such linking can expose a language to foreign behaviors that are internally inexpressible, which poses a serious threat to safety invariants and programmer reasoning. To preserve such invariants, a language may try to add features to limit the reliance on external libraries, but endless extensions can obscure the core abstractions the language was designed to provide.
In this paper, we outline an approach that encapsulates foreign code in a sound way—i.e., without disturbing the invariants promised by types of the core language. First, one introduces novel linking types that characterize the behaviors of foreign libraries that are inexpressible in the core language. To reason about the soundness of linking, one constructs a realizability model that captures the meaning of both core types and linking types as sets of target-language terms. Using this model, one can formally prove when foreign behavior is encapsulated; that is, unobservable to core code. We show one way to discharge such proofs automatically by augmenting the compiler to insert verified encapsulation wrappers around components that use foreign libraries.
Inspired by existing approaches to FFIs, we develop a pair of case studies that extend a pure, functional language: one extension for state, and another for exceptions. The first allows us to implement mutable references via a library, whereas the second allows us to implement try and catch as library functions. Both extensions and the overall system are proven sound using logical relations that use realizability techniques.
@InProceedings{TyDe23p14,
author = {Daniel Patterson and Andrew Wagner and Amal Ahmed},
title = {Semantic Encapsulation using Linking Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {14--28},
doi = {10.1145/3609027.3609405},
year = {2023},
}
Publisher's Version
TyDe '23: "Semantic Encapsulation using ..."
Semantic Encapsulation using Linking Types
Daniel Patterson, Andrew Wagner, and Amal Ahmed
(Northeastern University, USA)
Interoperability pervades nearly all mainstream language implementations, as most systems leverage subcomponents written in different languages. And yet, such linking can expose a language to foreign behaviors that are internally inexpressible, which poses a serious threat to safety invariants and programmer reasoning. To preserve such invariants, a language may try to add features to limit the reliance on external libraries, but endless extensions can obscure the core abstractions the language was designed to provide.
In this paper, we outline an approach that encapsulates foreign code in a sound way—i.e., without disturbing the invariants promised by types of the core language. First, one introduces novel linking types that characterize the behaviors of foreign libraries that are inexpressible in the core language. To reason about the soundness of linking, one constructs a realizability model that captures the meaning of both core types and linking types as sets of target-language terms. Using this model, one can formally prove when foreign behavior is encapsulated; that is, unobservable to core code. We show one way to discharge such proofs automatically by augmenting the compiler to insert verified encapsulation wrappers around components that use foreign libraries.
Inspired by existing approaches to FFIs, we develop a pair of case studies that extend a pure, functional language: one extension for state, and another for exceptions. The first allows us to implement mutable references via a library, whereas the second allows us to implement try and catch as library functions. Both extensions and the overall system are proven sound using logical relations that use realizability techniques.
@InProceedings{TyDe23p14,
author = {Daniel Patterson and Andrew Wagner and Amal Ahmed},
title = {Semantic Encapsulation using Linking Types},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {14--28},
doi = {10.1145/3609027.3609405},
year = {2023},
}
Publisher's Version
TyDe '23: "Infix-Extensible Record Types ..."
Infix-Extensible Record Types for Tabular Data
Adam Paszke and Ningning Xie
(Google DeepMind, Germany; Google DeepMind, Canada)
We present a novel row-polymorphic record calculus, supporting a unique combination of features: scoped labels, first-class labels and rows, and record concatenation. Our work is motivated by the similarity of record types and data table (or data frame) schemas, commonly used in data processing tasks. After presenting our record calculus, we demonstrate its applicability to data frame manipulation by showing that it can be used to successfully assign types to the functions listed in the Brown Benchmark for Tabular Types. Our typing discipline is remarkably lightweight, compared to calculi that require reasoning about type-level constraints when manipulating record types, making it a viable candidate for practical use.
@InProceedings{TyDe23p29,
author = {Adam Paszke and Ningning Xie},
title = {Infix-Extensible Record Types for Tabular Data},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {29--43},
doi = {10.1145/3609027.3609406},
year = {2023},
}
Publisher's Version
TyDe '23: "A Dependently Typed Language ..."
A Dependently Typed Language with Dynamic Equality
Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, and Hongwei Xi
(Autodesk, USA; Boston University, USA)
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories. We address this issue by designing a dependently typed language where equality checking is delayed until runtime. What were once static errors can now be presented to programmers as warnings. When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution. We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language. Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage. Finally, we have implemented a prototype of the language.
@InProceedings{TyDe23p44,
author = {Mark Lemay and Qiancheng Fu and William Blair and Cheng Zhang and Hongwei Xi},
title = {A Dependently Typed Language with Dynamic Equality},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {44--57},
doi = {10.1145/3609027.3609407},
year = {2023},
}
Publisher's Version
TyDe '23: "A Calculus of Inductive Linear ..."
A Calculus of Inductive Linear Constructions
Qiancheng Fu and Hongwei Xi
(Boston University, USA)
In this paper, we present a novel calculus of inductive linear constructions (CILC), combining linear types and dependent types. Our type theory addresses a looming issue in the research on linear dependent types: the lack of a general mechanism for defining sound linear inductive types. CILC allows one to encode in a straightforward manner the linear connectives that must be baked into the core of other systems. This greatly lowers the difficulty of encoding various data structures and makes writing non-trivial programs humanly feasible. We study the standard meta theory of our calculus, showing that it is sound in the usual sense. Through a heap-based operational semantics, we show that CILC safely manipulates resources and runs memory clean. We have formalized and proven correct most of the reported results in the Coq Proof Assistant.
@InProceedings{TyDe23p1,
author = {Qiancheng Fu and Hongwei Xi},
title = {A Calculus of Inductive Linear Constructions},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {1--13},
doi = {10.1145/3609027.3609404},
year = {2023},
}
Publisher's Version
Published Artifact
Artifacts Available
TyDe '23: "A Dependently Typed Language ..."
A Dependently Typed Language with Dynamic Equality
Mark Lemay, Qiancheng Fu, William Blair, Cheng Zhang, and Hongwei Xi
(Autodesk, USA; Boston University, USA)
Dependent type systems are powerful tools for preventing bugs in programs. Unlike other formal methods, dependent type systems can reuse the methodology and syntax familiar to functional programmers to construct formal proofs. However, usability issues, like confusing error messages, often arise from the conservative equalities required by such type theories. We address this issue by designing a dependently typed language where equality checking is delayed until runtime. What were once static errors can now be presented to programmers as warnings. When runtime failures occur, the blame system provides clear error messages indicating the exact static assumption violated during execution. We present several examples in this system, introduce novel correctness properties, and prove them for a fragment of the language. Our full system handles dependent indexed data and pattern matching, which are difficult for dependent gradual typing systems to manage. Finally, we have implemented a prototype of the language.
@InProceedings{TyDe23p44,
author = {Mark Lemay and Qiancheng Fu and William Blair and Cheng Zhang and Hongwei Xi},
title = {A Dependently Typed Language with Dynamic Equality},
booktitle = {Proc.\ TyDe},
publisher = {ACM},
pages = {44--57},
doi = {10.1145/3609027.3609407},
year = {2023},
}
Publisher's Version