Unified syntax with iso-types

DOI10.1007/978-3-319-47958-3_14MaRDI QIDQ3179296zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• Higher-order unification with dependent function types
• scientific article; zbMATH DE number 1678369
• scientific article; zbMATH DE number 761284
• : dependent types without the sugar
• Higher-order dynamic pattern unification for dependent types and records

Cites work

• scientific article; zbMATH DE number 1629944 (Why is no real title available?)
• Cayenne -- a language with dependent types
• Closed type families with overlapping equations
• Combining proofs and programs in a dependently typed language
• Efficient self-interpretation in lambda calculus
• Introduction to generalized type systems
• Programming up to congruence
• Pure type systems with judgemental equality
• Secure distributed programming with value-dependent types
• System FC with explicit kind equality
• The calculus of constructions
• Types and programing languages
• Typing in pure type systems
• Unified syntax with iso-types
• : dependent types without the sugar

Cited in

(1)

• Unified syntax with iso-types

Describes a project that uses

Uses Software

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

This page was built for publication: Unified syntax with iso-types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179296)