scientific article; zbMATH DE number 3859117
From MaRDI portal
Publication:3328540
Recommendations
Cited in
(82)- Univalent Foundations and the UniMath Library
- Some normalization properties of Martin-Löf's type theory, and applications
- Topological quantum gates in homotopy type theory
- The concept \textit{horse} is a concept
- scientific article; zbMATH DE number 53194 (Why is no real title available?)
- Internal parametricity for cubical type theory
- Constructive Mathematics and Functional Programming (Abstract)
- RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
- Eta-rules in Martin-Löf type theory
- Theory of Constructive Semigroups with Apartness – Foundations, Development and Practice
- Cubical methods in homotopy type theory and univalent foundations
- scientific article; zbMATH DE number 130887 (Why is no real title available?)
- Type theory as a foundation for computer science
- A comparison of HOL and ALF formalizations of a categorical coherence theorem
- Importing mathematics from HOL into Nuprl
- W-types in setoids
- Categories with families: unityped, simply typed, and dependently typed
- A generic algebra for data collections based on constructive logic
- Programming by example and proving by example using higher-order unification
- A proposal for broad spectrum proof certificates
- Applications of type theory
- An introduction to univalent foundations for mathematicians
- Process calculus based upon evaluation to committed form
- A Comparison of Type Theory with Set Theory
- Natural Deduction for Equality: The Missing Entity
- On the relationship between foundations of programming and mathematics
- Truth and proof in intuitionism
- Intuitionistic completeness of first-order logic
- scientific article; zbMATH DE number 4006266 (Why is no real title available?)
- Constructive Mathematics in Theory and Programming Practice
- A small complete category
- Using formal methods with SysML in aerospace design and engineering
- Insight in discrete geometry and computational content of a discrete model of the continuum
- Middle-out reasoning for synthesis and induction
- Formally computing with the non-computable
- The practice of logical frameworks
- Homotopy type theory and Voevodsky's univalent foundations
- Martin-Löf identity types in C-systems
- POPLMark reloaded: mechanizing proofs by logical relations
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Finitary type theories with and without contexts
- Exploring abstract algebra in constructive type theory
- From signatures to monads in \textsf{UniMath}
- Turing-Completeness Totally Free
- Applause: An implementation of the Collins-Michalski theory of plausible reasoning
- Proof-search in type-theoretic languages: An introduction
- Constructive system for automatic program synthesis
- A meaning explanation for HoTT
- A higher-order interpretation of deductive tableau
- The origins of structural operational semantics
- From type theory to setoids and back
- Intuitionistic ancestral logic as a dependently typed abstract programming language
- Predicativity and constructive mathematics
- Towards a directed homotopy type theory
- A characterisation of elementary fibrations
- scientific article; zbMATH DE number 3936476 (Why is no real title available?)
- Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
- The justification of identity elimination in Martin-Löf's type theory
- Between constructive mathematics and PROLOG
- Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
- Constructive algebraic integration theory
- A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis
- Induction-recursion and initial algebras.
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- Static semantics, types, and binding time analysis
- An adequacy theorem for dependent type theory
- Program testing and the meaning explanations of intuitionistic type theory
- On the proof theory of Coquand's calculus of constructions
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
- Connectionist computations of intuitionistic reasoning
- scientific article; zbMATH DE number 3894466 (Why is no real title available?)
- From mathesis universalis to provability, computability, and constructivity
- Constructivity in computer science. Summer symposium, San Antonio, TX, June 19--22, 1991. Proceedings
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- Some points in formal topology.
- Partial inductive definitions
- Nonconstructive computational mathematics
- Coalgebras in functional programming and type theory
- A type-theoretic approach to program development
- IMPS: An interactive mathematical proof system
- A computer-verified monadic functional implementation of the integral
- A Classical Realizability Model for a Semantical Value Restriction
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3328540)
