Contextual modal type theory
From MaRDI portal
Publication:5277812
DOI10.1145/1352582.1352591zbMath1367.03060MaRDI QIDQ5277812
Brigitte Pientka, Frank Pfenning, Aleksandar Nanevski
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1028.3796
03B45: Modal logic (including the logic of norms)
68N18: Functional programming and lambda calculus
03B70: Logic in computer science
68N17: Logic programming
Related Items
Two-level Lambda-calculus, Coalgebras as Types Determined by Their Elimination Rules, A Logical Foundation for Environment Classifiers, J-Calc: a typed lambda calculus for intuitionistic justification logic, Intuitionistic hypothetical logic of proofs, The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey, A modal type theory for formalizing trusted communications, Hypothetical logic of proofs, A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, Explicit Contexts in LF (Extended Abstract), Case Analysis of Higher-Order Data, Functional Programming With Higher-order Abstract Syntax and Explicit Substitutions, Modalities Without Worlds, Programs Using Syntax with First-Class Binders, LINCX: A Linear Logical Framework with First-Class Contexts, Higher-Order Dynamic Pattern Unification for Dependent Types and Records, Programming Inductive Proofs, Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables, Refined Environment Classifiers, Inductive Beluga: Programming Proofs, Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
Uses Software
