scientific article; zbMATH DE number 7453169

MaRDI QIDQ5020623

Christopher Jenkins, Larry Diehl, Aaron Stump

Publication date: 6 January 2022

Full work available at URL: https://arxiv.org/abs/2005.00199

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Innovations in computational type theory using Nuprl
• The calculus of constructions
• A discrimination algorithm inside \(\lambda -\beta\)-calculus
• Efficient Mendler-style lambda-encodings in Cedille
• A fixpoint theorem for complete categories
• From realizability to induction via dependent intersection
• Inductive types and type constraints in the second-order lambda calculus
• A lattice-theoretical fixpoint theorem and its applications
• Type fixpoints
• Copatterns
• Type-based termination of recursive definitions
• Monotone (co)inductive types and positive fixed-point types
• Wellfounded recursion with copatterns
• Safe zero-cost coercions for Haskell
• The calculus of dependent lambda eliminations

This page was built for publication: