Extensional equivalence and singleton types

DOI10.1145/1183278.1183281zbMath1367.68055OpenAlexW2161017670MaRDI QIDQ5277760

Robert Harper, Christopher A. Stone

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1183278.1183281

zbMATH Keywords

logical relationssingleton typesequivalence algorithms

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Related Items (9)

Certifying data in multiparty session types ⋮ Equality Checking for General Type Theories in Andromeda 2 ⋮ Certifying Data in Multiparty Session Types ⋮ An extensible equality checking algorithm for dependent type theories ⋮ 1ML – Core and modules united ⋮ Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions ⋮ Unnamed Item ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ F-ing modules

This page was built for publication: Extensional equivalence and singleton types