Is Impredicativity Implicitly Implicit

DOI10.4230/lipics.types.2019.9OpenAlexW3169999972MaRDI QIDQ6079240

Unnamed Author, Stefan Monnier

Publication date: 27 October 2023

Full work available at URL: https://drops.dagstuhl.de/opus/volltexte/2020/13073/pdf/LIPIcs-TYPES-2019-9.pdf/

zbMATH Keywords

pure type systemsinductive typesimpredicativityproof irrelevanceimplicit argumentsuniverse polymorphismerasable arguments

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proofs for free
• On Irrelevance and Algorithmic Equality in Predicative Type Theory
• A Brief Overview of Agda – A Functional Language with Dependent Types
• (In)consistency of Extensions of Higher Order Logic and Type Theory
• On the Strength of Proof-Irrelevant Type Theories
• Introduction to generalized type systems
• Parametric higher-order abstract syntax for mechanized semantics
• Cayenne—a language with dependent types
• Impredicative Concurrent Abstract Predicates
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Erasure and Polymorphism in Pure Type Systems
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types

This page was built for publication: Is Impredicativity Implicitly Implicit