Article

Lambda-My-Calculus: An Algorithmic Interpretation of Classical Natural Deduction

Author:

Michel ParigotAuthors Info & Claims

LPAR '92: Proceedings of the International Conference on Logic Programming and Automated Reasoning

Pages 190 - 201

Published: 15 July 1992 Publication History

Abstract

No abstract available.

Cited By

View all

Barenbaum PFreund TGorla D(2021)A constructive logic with classical proofs and refutationsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470649(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470649
Hirsch ATate R(2018)Strict and lazy semantics for effects: layering monads and comonadsProceedings of the ACM on Programming Languages10.1145/32367832:ICFP(1-30)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236783
Cong YAsai K(2018)Handling delimited continuations with dependent typesProceedings of the ACM on Programming Languages10.1145/32367642:ICFP(1-31)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236764
Show More Cited By

Recommendations

Focused Linear Logic and the λ-calculus

Linear logic enjoys strong symmetries inherited from classical logic while providing a constructive framework comparable to intuitionistic logic. However, the computational interpretation of sequent calculus presentations of linear logic remains ...
The safe lambda calculus
TLCA'07: Proceedings of the 8th international conference on Typed lambda calculi and applications

Safety is a syntactic condition of higher-order grammars that constrains occurrences of variables in the production rules according to their type-theoretic order. In this paper, we introduce the safe lambda calculus, which is obtained by transposing (...
The λ-Calculus and the Unity of Structural Proof Theory
Special Issue: Computation and Logic in the Real World; Guest Editors: S. Barry Cooper, Elvira Mayordomo and Andrea Sorbi

In the context of intuitionistic implicational logic, we achieve a perfect correspondence (technically an isomorphism) between sequent calculus and natural deduction, based on perfect correspondences between left-introduction and elimination, cut and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

LPAR '92: Proceedings of the International Conference on Logic Programming and Automated Reasoning

July 1992

609 pages

ISBN:354055727X

Editor:
Andrei Voronkov

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 15 July 1992

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

131
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Barenbaum PFreund TGorla D(2021)A constructive logic with classical proofs and refutationsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470649(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470649
Hirsch ATate R(2018)Strict and lazy semantics for effects: layering monads and comonadsProceedings of the ACM on Programming Languages10.1145/32367832:ICFP(1-30)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236783
Cong YAsai K(2018)Handling delimited continuations with dependent typesProceedings of the ACM on Programming Languages10.1145/32367642:ICFP(1-31)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236764
Bakel S(2018)Characterisation of Normalisation Properties for λμ using Strict Negated Intersection TypesACM Transactions on Computational Logic10.1145/314982319:1(1-47)Online publication date: 15-Feb-2018
https://dl.acm.org/doi/10.1145/3149823
Santo JGhilezan SVanhoof WPientka B(2017)Characterization of strong normalizability for a sequent lambda calculus with co-controlProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming10.1145/3131851.3131867(163-174)Online publication date: 9-Oct-2017
https://dl.acm.org/doi/10.1145/3131851.3131867
Geuvers HHurkens T(2017)Deriving Natural Deduction Rules from Truth TablesProceedings of the 7th Indian Conference on Logic and Its Applications - Volume 1011910.1007/978-3-662-54069-5_10(123-138)Online publication date: 5-Jan-2017
https://dl.acm.org/doi/10.1007/978-3-662-54069-5_10
Pédrot PSaurin A(2016)Classical By-NeedProceedings of the 25th European Symposium on Programming Languages and Systems - Volume 963210.5555/3089528.3089552(616-643)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.5555/3089528.3089552
Downen PMaurer LAriola ZPeyton Jones S(2016)Sequent calculus as a compiler intermediate languageACM SIGPLAN Notices10.1145/3022670.295193151:9(74-88)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951931
Cauderlier RAlves SDowek GLicata D(2016)A Rewrite System for Proof ConstructivizationProceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice10.1145/2966268.2966270(1-7)Online publication date: 23-Jun-2016
https://dl.acm.org/doi/10.1145/2966268.2966270
Downen PMaurer LAriola ZPeyton Jones SGarrigue JKeller GSumii E(2016)Sequent calculus as a compiler intermediate languageProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951931(74-88)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951931
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

Cited By

Recommendations

Focused Linear Logic and the λ-calculus

The safe lambda calculus

The λ-Calculus and the Unity of Structural Proof Theory

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Get Access

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations