A Lambda Calculus Based on Quantum Logic
We propose a typed lambda calculus based on quantum logic. We first present a natural deduction system for quantum logic with the Sasaki hook as its implication operation and then formulate a typed lambda calculus connected to this system through the Curry-Howard correspondence. We prove soundness and completeness of the former with respect to orthomodular lattices and strong normalization of the latter. The resulting lambda calculus has the characteristic feature that only one assumption is available in the typing derivation that serves as the premise of $λ$-abstraction. Under this…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2610.34266
curl -X POST /api/v1/records/arxiv/2610.34266/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.34266/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'