I Got Plenty o’ Nuttin’
From MaRDI portal
Publication:3188289
DOI10.1007/978-3-319-30936-1_12zbMath1343.68060OpenAlexW2484189767MaRDI QIDQ3188289
Publication date: 17 August 2016
Published in: A List of Successes That Can Change the World (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-30936-1_12
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (9)
Linear Dependent Type Theory for Quantum Programming Languages ⋮ Additive types in quantitative type theory ⋮ A dependent dependency calculus ⋮ A Java-like calculus with heterogeneous coeffects ⋮ Observed Communication Semantics for Classical Processes ⋮ Graded modal dependent type theory ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ Unnamed Item ⋮ \( \pi\) with leftovers: a mechanisation in Agda
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- A linear logical framework
- Some lambda calculus and type theory formalized
- Coeffects
- Integrating Linear and Dependent Types
- Proofs for free
- A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
- Linear dependent types for differential privacy
- Proof-Carrying Code in a Session-Typed Process Calculus
- Pure type systems with judgemental equality
- Session Types as Intuitionistic Linear Propositions
- Propositions as sessions
- Linear type theory for asynchronous session types
- Fun with semirings
- Secure distributed programming with value-dependent types
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Types for Proofs and Programs
- Parallel reductions in \(\lambda\)-calculus
This page was built for publication: I Got Plenty o’ Nuttin’
