Automorphisms of types in certain type theories and representation of finite groups

DOI10.1017/S0960129518000129zbMath1456.03028MaRDI QIDQ3119463

Serguei V. Solov'ev

Publication date: 12 March 2019

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129518000129

Mathematics Subject Classification ID

20C15: Ordinary representations and characters

68N18: Functional programming and lambda calculus

03B40: Combinatory logic and lambda calculus

Related Items

Automorphisms of types and their applications

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nonabelian algebraic topology. Filtered spaces, crossed complexes, cubical homotopy groupoids. With contributions by Christopher D. Wensley and Sergei V. Soloviev
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The calculus of constructions
• Characterization of normal forms possessing inverse in the \(\lambda\)- \(\beta\)-\(\eta\)-calculus
• The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus
• The category of finite sets and Cartesian closed categories
• Coercive subtyping: theory and implementation
• Remarks on isomorphisms in typed lambda calculi with empty and sum types
• Kombinatorische Anzahlbestimmungen für Gruppen, Graphen und chemische Verbindungen
• Isomorphisms of types in the presence of higher-order references (extended version)
• A computational view of implicit coercions in type theory
• Isomorphisms of generic recursive polynomial types
• Provable isomorphisms of types
• Topology and logic as a source of algebra
• Isomorphic objects in symmetric monoidal closed categories
• Isomorphism of intersection and union types
• Proof Systems for Retracts in Simply Typed Lambda Calculus
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Graphs of Degree Three with a Given Abstract Group
• Coercion completion and conservativity in coercive subtyping