Unified Syntax with Iso-types

DOI10.1007/978-3-319-47958-3_14zbMath1483.68065OpenAlexW2527749908MaRDI QIDQ3179296

Bruno C. d. S. Oliveira, Yanpeng Yang, Xuan Bi

Publication date: 21 December 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-47958-3_14

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Related Items (1)

Unified Syntax with Iso-types

Uses Software

• Coq
• Automath
• Cayenne
• Irdis
• Idris
• F*

Cites Work

• Unnamed Item
• Unnamed Item
• The calculus of constructions
• Typing in pure type systems
• Programming up to Congruence
• Unified Syntax with Iso-types
• Pure type systems with judgemental equality
• ΠΣ: Dependent Types without the Sugar
• Efficient self-interpretation in lambda calculus
• Introduction to generalized type systems
• Secure distributed programming with value-dependent types
• System FC with explicit kind equality
• Cayenne—a language with dependent types
• Combining proofs and programs in a dependently typed language
• Closed type families with overlapping equations

This page was built for publication: Unified Syntax with Iso-types