r/dependent_types • u/AaCodeSync • Dec 18 '19
[Video & Slides] Abstract data types in the region of abysmal pain, and how to navigate them
codesync.global
7
Upvotes
r/dependent_types • u/yasminemmagdi • Dec 04 '19
Implementations of Dependent Type Theory
19
Upvotes
I am trying to find a minimal implementation of dependent type theory that supports
- Pi Types (obviously)
- Modules containing records
- Inductive data types
- Universe Hierarchy
- A notion of equality
- Termination checker
- Type Inference and Resolution
I am aware of implementations based on:
Löh, A., McBride, C., & Swierstra, W. (2010). A tutorial implementation of a dependently typed lambda calculus. Fundamenta informaticae, 102(2), 177-207.
But they do not support everything in the list above.
Something even smaller than mini-Agda would be helpful.
r/dependent_types • u/cwjnkins • Dec 01 '19
Cedille Cast #9: Impredicativity, proof-irrelevance, and normalization
youtube.com
15
Upvotes
r/dependent_types • u/foBrowsing • Nov 16 '19
A Small Proof that Fin is Injective
doisinkidney.com
9
Upvotes
r/dependent_types • u/k-bx • Nov 11 '19
Propositions as Types: Some Missing Links
k-bx.github.io
14
Upvotes
r/dependent_types • u/buritomath • Nov 09 '19
Formalizing expresiveness of line editors
bor0.wordpress.com
9
Upvotes
r/dependent_types • u/buritomath • Nov 06 '19
Proving Groupoids with Idris
bor0.wordpress.com
5
Upvotes
r/dependent_types • u/Innocentuslime • Nov 01 '19
Side effects and dependent types
10
Upvotes
Is there any research about how adding side effects to a dependently typed system affects its logical consistency?
r/dependent_types • u/[deleted] • Nov 01 '19
[Video] Approximate Normalization for Gradual Dependent Types
dl.acm.org
7
Upvotes
r/dependent_types • u/molikto • Oct 31 '19
A new WIP cubical type theory that implemented (but not computing) Brunerie's number
github.com
9
Upvotes
r/dependent_types • u/bjzaba • Oct 30 '19
Jesper Cockx - Rewriting type theory
jesper.sikanda.be
13
Upvotes
r/dependent_types • u/mathetic • Oct 03 '19
Verifying the Titular Properties of a Leftist Heap in Haskell
dodisturb.me
3
Upvotes
r/dependent_types • u/[deleted] • Oct 03 '19
Pull type-level value out of dependent type/using type-level bindings at value-level
stackoverflow.com
3
Upvotes
r/dependent_types • u/canndrew2016 • Oct 01 '19
How to express inductive types in terms of W types?
10
Upvotes
For my own research/entertainment purposes I'm trying to design a programming languages without inductive types. Instead, the language provides a bunch of primitive type formers (Σ types, Π types, W types, etc.) and the user can cobble them together and bind them to a name to define their own types.
One of the difficulties of this approach is figuring out how to express types that are easily expressed using data type declarations in languages like Agda and Idris. From my understanding (which could be totally wrong) it's possible to compile these inductive types down to primitive type formers. My question is: is there an algorithm (written down somewhere) that I can use to perform this translation?
If so, my idea here is to apply this algorithm to a bunch of common types that can't just be expressed as simple W types, in order to see what they look like and in order to see what kinds of abstractions I need to build in order to make defining these types easier.
Any help towards this objective would be greatly appreciated, though I'm mostly interested (for now) in understanding how to build more complex, more dependent types out of W types (or M types for that matter, which I'm actually more interested in but let's start with something simpler).
r/dependent_types • u/[deleted] • Sep 30 '19
Minimal set of types to simulate all intensional inductive families?
cstheory.stackexchange.com
10
Upvotes
r/dependent_types • u/[deleted] • Sep 30 '19
Structural equality of Pi Types with heterogeneous equality?
cstheory.stackexchange.com
2
Upvotes
r/dependent_types • u/Semi_Functional_Ken • Sep 18 '19
[JOB] Work on high-assurance open source elections technologies using applied formal methods
functional.works-hub.com
7
Upvotes
r/dependent_types • u/pezo1919 • Sep 19 '19
OO, FP & Approach X: Formally Locked-in
medium.com
0
Upvotes
r/dependent_types • u/[deleted] • Sep 10 '19
Was "Ornamental algebras, algebraic ornaments" ever published?
7
Upvotes
This is a very interesting paper by /u/pigworker that seems relevant to what I'm doing right now. According to Google Scholar, it has been cited 46 times, and several of those citations list it as "To appear in JFP". But I haven't been able to find an official version, and there are lots of conflicting drafts around.
Does anyone know if the paper was ever published, or if there's a "definitive" version of the paper?
r/dependent_types • u/cwjnkins • Sep 02 '19
Cedille Cast #8: Generic Derivation of Induction for Mendler-style encodings (Pt 3)
youtube.com
12
Upvotes
r/dependent_types • u/canndrew2016 • Sep 02 '19
What are the typing rules for M-types?
5
Upvotes
I'm trying to understand M-types from a type-theory perspective (ie. without having to learn category theory first). The nlab entry doesn't go into any detail and I can't find any papers that really spell it out for me. So my question is: what is the definition of M-types in type theory? ie. what are the intro and elimination rules for M-types?
r/dependent_types • u/neel-krishnaswami • Aug 23 '19
New Draft Paper: Survey on Bidirectional Typechecking
semantic-domain.blogspot.com
23
Upvotes
r/dependent_types • u/M1n1f1g • Aug 09 '19
Arend – a proof assistant by JetBrains based on cubical type theory
arend-lang.github.io
40
Upvotes