Search results for "Curry-Howard"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
123	Jean-Louis Krivine	The Curry-Howard Correspondence in Set Theory.	LICS	2000	DBLP DOI BibTeX RDF
115	Tim Sheard	Putting curry-howard to work.	Haskell	2005	DBLP DOI BibTeX RDF	extensional kind system, logic, haskell, GADT, curry-howard isomorphism
99	Iman Poernomo, John N. Crossley, Martin Wirsing	Programs, Proofs and Parametrized Specifications.	WADT	2001	DBLP DOI BibTeX RDF	Parametrized specifications, CASL, SML, Curry-Howard isomorphism
85	Kostia Chardonnet	Towards a Curry-Howard Correspondence for Quantum Computation. (Vers une correspondance de Curry-Howard pour le calcul quantique).		2023	RDF
85	Farzad Jafarrahmani	Fixpoints of Types in Linear Logic from a Curry-Howard-Lambek Perspective. (Points fixes de types en logique linéaire d'un point de vue Curry-Howard-Lambek).		2023	RDF
73	Neelakantan R. Krishnaswami	Focusing on pattern matching.	POPL	2009	DBLP DOI BibTeX RDF	curry-howard, pattern matching, type theory, focusing
73	Jean-Louis Krivine	A call-by-name lambda-calculus machine.	High. Order Symb. Comput.	2007	DBLP DOI BibTeX RDF	Lambda-calculus machine, Control instruction, Curry-Howard correspondence
73	Atsushi Ohori	A proof theory for machine code.	ACM Trans. Program. Lang. Syst.	2007	DBLP DOI BibTeX RDF	Curry-Howard isomorphism
73	Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori	Pure patterns type systems.	POPL	2003	DBLP DOI BibTeX RDF	Curry-Howard, pure type systems, patterns, matching, logics, Lambda-calculus, rewriting
69	Murdoch Gabbay, Dominic P. Mulligan	One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations.	WoLLIC	2008	DBLP DOI BibTeX RDF
69	Atsushi Ohori	A Curry-Howard Isomorphism for Compilation and Program Execution.	TLCA	1999	DBLP DOI BibTeX RDF
54	Ana Bove, Peter Dybjer	Dependent Types at Work.	LerNet ALFA Summer School	2008	DBLP DOI BibTeX RDF
54	Herman Geuvers, Rob Nederpelt	Rewriting for Fitch Style Natural Deductions.	RTA	2004	DBLP DOI BibTeX RDF
54	François Maurel	Nondeterministic Light Logics and NP-Time.	TLCA	2003	DBLP DOI BibTeX RDF	Light logics, implicit characterisations of complexity classes, NP complexity
54	Jean-Louis Krivine	Typed lambda-calculus in classical Zermelo-Frænkel set theory.	Arch. Math. Log.	2001	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000): 03E40, 03B40, 68N18
54	Iman Poernomo, John N. Crossley	Protocols between Programs and Proofs.	LOPSTR (LNCS 2042: Selected Papers)	2000	DBLP DOI BibTeX RDF
54	Torben Braüner	The Girard Translation Extended with Recursion.	CSL	1994	DBLP DOI BibTeX RDF
53	Noam Zeilberger	Refinement types and computational duality.	PLPV	2009	DBLP DOI BibTeX RDF	duality, effects, intersection types, focusing, union types
46	Zena M. Ariola, Aaron Bohannon, Amr Sabry	Sequent calculi and abstract machines.	ACM Trans. Program. Lang. Syst.	2009	DBLP DOI BibTeX RDF	Krivine machine, duality, explicit substitutions, natural deduction, Curry-Howard isomorphism
46	Harry Halpin	From Typed-Functional Semantic Web Services to Proofs.	ISWC	2006	DBLP DOI BibTeX RDF	Functional Programming, Semantic Web Services, Type Theory, Proofs, Curry-Howard Isomorphism
46	Yosihiro Yuse, Atsushi Igarashi	A modal type system for multi-level generating extensions with persistent code.	PPDP	2006	DBLP DOI BibTeX RDF	time-ordered normalization, temporal logic, type systems, modal logic, meta-programming, curry-howard isomorphism
46	Pavel Naumov	On Modal Logics of Partial Recursive Functions.	Stud Logica	2005	DBLP DOI BibTeX RDF	modal logic, recursive function, Curry-Howard isomorphism
46	Philip Wadler	Call-by-value is dual to call-by-name.	ICFP	2003	DBLP DOI BibTeX RDF	Curry-Howard correspondence, De Morgan dual, lambda mu calculus, logic, lambda calculus, sequent calculus, natural deduction
46	Uday S. Reddy	A Typed Foundation for Directional Logic Programming.	ELP	1992	DBLP DOI BibTeX RDF	Directionality, types, linear logic, sequent calculus, modes, concurrent logic programming, Curry-Howard isomorphism, logic variables
42	Juan Climent Vidal, Enric Cosme-Llópez	From higher-order rewriting systems to higher-order categorial algebras and higher-order Curry-Howard isomorphisms.	CoRR	2024	DBLP DOI BibTeX RDF
42	Kostia Chardonnet, Alexis Saurin, Benoît Valiron	A Curry-Howard Correspondence for Linear, Reversible Computation.	CoRR	2023	DBLP DOI BibTeX RDF
42	Kostia Chardonnet, Alexis Saurin, Benoît Valiron	A Curry-Howard Correspondence for Linear, Reversible Computation.	CSL	2023	DBLP DOI BibTeX RDF
42	Ivo Pezlar	The placeholder view of assumptions and the Curry-Howard correspondence.	Synth.	2021	DBLP DOI BibTeX RDF
42	Cosimo Perini Brogi	Curry-Howard-Lambek Correspondence for Intuitionistic Belief.	Stud Logica	2021	DBLP DOI BibTeX RDF
42	Ivo Pezlar	The Placeholder View of Assumptions and the Curry-Howard Correspondence (Extended Abstract).	CLAR	2021	DBLP DOI BibTeX RDF
42	Cosimo Perini Brogi	Curry-Howard-Lambek Correspondence for Intuitionistic Belief.	CoRR	2020	DBLP BibTeX RDF
42	Kostia Chardonnet, Alexis Saurin, Benoît Valiron	Toward a Curry-Howard Equivalence for Linear, Reversible Computation - Work-in-Progress.	RC	2020	DBLP DOI BibTeX RDF
42	Juan Ferrer Meleiro, Hugo Luiz Mariano	Formalizing the Curry-Howard Correspondence.	CoRR	2019	DBLP BibTeX RDF
42	Cécilia Pradic, Colin Riba	A Curry-Howard Approach to Church's Synthesis.	Log. Methods Comput. Sci.	2019	DBLP DOI BibTeX RDF
42	Federico Aschieri, Agata Ciabattoni, Francesco A. Genco	Disjunctive Axioms and Concurrent λ-Calculi: a Curry-Howard Approach.	CoRR	2018	DBLP BibTeX RDF
42	Rob Arthan, Paulo Oliva	A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz Logic.	CoRR	2018	DBLP BibTeX RDF
42	Cécilia Pradic, Colin Riba	A Curry-Howard Approach to Church's Synthesis.	CoRR	2018	DBLP BibTeX RDF
42	Cécilia Pradic, Colin Riba	LMSO: A Curry-Howard Approach to Church's Synthesis via Linear Logic.	LICS	2018	DBLP DOI BibTeX RDF
42	Konstantinos Pouliasis	Relating Justification Logic Modality and Type Theory in Curry-Howard Fashion.		2018	RDF
42	Cécilia Pradic, Colin Riba	A Curry-Howard Approach to Church's Synthesis.	FSCD	2017	DBLP DOI BibTeX RDF
42	Federico Aschieri, Margherita Zorzi	On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem.	Theor. Comput. Sci.	2016	DBLP DOI BibTeX RDF
42	G. A. Kavvos	The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time.	CoRR	2016	DBLP BibTeX RDF
42	Lucius Schoenbaum	A Generalization of the Curry-Howard Correspondence.	CoRR	2016	DBLP BibTeX RDF
42	Johannes Emerich	How Are Programs Found? Speculating About Language Ergonomics With Curry-Howard.	CoRR	2016	DBLP BibTeX RDF
42	Federico Aschieri, Agata Ciabattoni, Francesco A. Genco	Curry-Howard Correspondence for Gödel Logic: from Natural Deduction to Parallel Computation.	CoRR	2016	DBLP BibTeX RDF
42	Federico Aschieri, Matteo Manighetti	On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic.	CoRR	2016	DBLP BibTeX RDF
42	Federico Aschieri	On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC.	Log. Methods Comput. Sci.	2016	DBLP DOI BibTeX RDF
42	Konstantinos Pouliasis	A Curry-Howard View of Basic Justification Logic.	WoLLIC	2016	DBLP DOI BibTeX RDF
42	Johannes Emerich	How are programs found? speculating about language ergonomics with Curry-Howard.	Onward!	2016	DBLP DOI BibTeX RDF
42	Federico Aschieri, Matteo Manighetti	On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic.	TYPES	2016	DBLP DOI BibTeX RDF
42	José Espírito Santo	Curry-Howard for Sequent Calculus at Last!.	TLCA	2015	DBLP DOI BibTeX RDF
42	Martín Hötzel Escardó, Chuangjie Xu	The Inconsistency of a Brouwerian Continuity Principle with the Curry-Howard Interpretation.	TLCA	2015	DBLP DOI BibTeX RDF
42	Pimpen Vejjajiva	Extended Curry-Howard terms for second-order logic.	Math. Log. Q.	2013	DBLP DOI BibTeX RDF
42	Marco Benini	Intuitionistic First-Order Logic: Categorical Semantics via the Curry-Howard Isomorphism.	CoRR	2013	DBLP BibTeX RDF
42	Federico Aschieri, Stefano Berardi, Giovanni Birolo	Realizability and Strong Normalization for a Curry-Howard Interpretation of HA + EM1.	CSL	2013	DBLP DOI BibTeX RDF
42	Murdoch James Gabbay, Dominic P. Mulligan	Corrigendum to "Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms" [Inf.Comput.208(3)(2010) 230-258].	Inf. Comput.	2012	DBLP DOI BibTeX RDF
42	Murdoch James Gabbay, Dominic P. Mulligan	Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms.	Inf. Comput.	2010	DBLP DOI BibTeX RDF
42	Karl Mazurak, Steve Zdancewic	Lolliproc: to concurrency from classical linear logic via curry-howard and control.	ICFP	2010	DBLP DOI BibTeX RDF
42	Robert J. Irwin	Review of "Derivation and Computation: Taking the Curry-Howard Correspondence Seriously by Harold Simmons, " Cambridge University Press, 2000.	SIGACT News	2008	DBLP DOI BibTeX RDF
42	Alexander J. Summers	Curry-Howard Term Calculi for Gentzen-Style Classical Logics.		2008	RDF
42	Iman Hafiz Poernomo, Martin Wirsing, John Newsome Crossley	Adapting Proofs-as-Programs - The Curry-Howard Protocol		2005	DOI RDF
42	Alexandre Miquel	A Strongly Normalising Curry-Howard Correspondence for IZF Set Theory.	CSL	2003	DBLP DOI BibTeX RDF
42	Michael Florentin Nielsen	Modal logic and the Curry-Howard isomorphism.		1999	RDF
42	Atsushi Ohori	The Logical Abstract Machine: A Curry-Howard Isomorphism for Machine Code.	Fuji International Symposium on Functional and Logic Programming	1999	DBLP DOI BibTeX RDF
42	Frank A. Bäuerle, David W. Albrecht, John N. Crossley, John S. Jeavons	Curry-Howard Terms for Linear Logic.	Stud Logica	1998	DBLP DOI BibTeX RDF
42	David W. Albrecht, John N. Crossley, John S. Jeavons	New Curry-Howard Terms for Full Linear Logic.	Theor. Comput. Sci.	1997	DBLP DOI BibTeX RDF
42	C.-H. Luke Ong, Charles A. Stewart	A Curry-Howard Foundation for Functional Computation with Control.	POPL	1997	DBLP DOI BibTeX RDF	ML
42	Dov M. Gabbay, Ruy J. G. B. de Queiroz	Extending the Curry-Howard Interpretation to Linear, Relevant and Other Resource Logics.	J. Symb. Log.	1992	DBLP DOI BibTeX RDF
40	Michael Moortgat	Symmetries in Natural Language Syntax and Semantics: The Lambek-Grishin Calculus.	WoLLIC	2007	DBLP DOI BibTeX RDF
27	Takeshi Tsukada, Atsushi Igarashi	A Logical Foundation for Environment Classifiers.	TLCA	2009	DBLP DOI BibTeX RDF
27	Benoît Montagu, Didier Rémy	Modeling abstract types in modules with open existential types.	POPL	2009	DBLP DOI BibTeX RDF	linear type systems, modularity, generativity, type systems, modules, lambda-calculus, abstract types, existential types
27	Ruy J. G. B. de Queiroz	On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics.	Stud Logica	2008	DBLP DOI BibTeX RDF	reduction rules, proof-terms, proof-theoretic semantics, game-theoretic semantics, dialogue semantics, natural deduction
27	Daniel R. Licata, Noam Zeilberger, Robert Harper 0001	Focusing on Binding and Computation.	LICS	2008	DBLP DOI BibTeX RDF	computation, binding, logical frameworks, polarity, sequent calculus
27	Noam Zeilberger	Focusing and higher-order abstract syntax.	POPL	2008	DBLP DOI BibTeX RDF	pattern-matching, higher-order abstract syntax, focusing
27	Satoshi Kobayashi	A New Translation for Semi-classical Theories - Backtracking without CPS.	FLOPS	2008	DBLP DOI BibTeX RDF
27	Raffaella Bernardi, Michael Moortgat	Continuation Semantics for Symmetric Categorial Grammar.	WoLLIC	2007	DBLP DOI BibTeX RDF
27	José Espírito Santo	Completing Herbelin's Programme.	TLCA	2007	DBLP DOI BibTeX RDF
27	Yoshihiko Kakutani	Call-by-Name and Call-by-Value in Normal Modal Logic.	APLAS	2007	DBLP DOI BibTeX RDF
27	Thorsten Altenkirch, Conor McBride, Wouter Swierstra	Observational equality, now!	PLPV	2007	DBLP DOI BibTeX RDF	type theory, equality
27	Tim Sheard, Nathan Linger	Programming in Omega.	CEFP	2007	DBLP DOI BibTeX RDF
27	Anna Zamansky, Nissim Francez, Yoad Winter	A 'Natural Logic' inference system using the Lambek calculus.	J. Log. Lang. Inf.	2006	DBLP DOI BibTeX RDF	Natural logic, Inference, Normalization, Lambek calculus
27	James McKinna	Why dependent types matter.	POPL	2006	DBLP DOI BibTeX RDF
27	Alexander J. Summers, Steffen van Bakel	Approaches to Polymorphism in Classical Sequent Calculus.	ESOP	2006	DBLP DOI BibTeX RDF
27	Roy Dyckhoff, Delia Kesner, Stéphane Lengrand	Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic.	IJCAR	2006	DBLP DOI BibTeX RDF
27	Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz	Consistency and Completeness of Rewriting in the Calculus of Constructions.	IJCAR	2006	DBLP DOI BibTeX RDF
27	Peter Hines	Physical Systems as Constructive Logics.	UC	2006	DBLP DOI BibTeX RDF
27	Wojciech Moczydlowski	Normalization of IZF with Replacement.	CSL	2006	DBLP DOI BibTeX RDF
27	Alexis Saurin	Separation with Streams in the lambdaµ-calculus.	LICS	2005	DBLP DOI BibTeX RDF	Böhm Theorem, Calculus of Streams, Separation Property, Untyped ??-calculus
27	Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne	Characterizing strong normalization in a language with control operators.	PPDP	2004	DBLP DOI BibTeX RDF	functional programming, continuations, classical logic, intersection type
27	Jonathan Moody	Logical Mobility and Locality Types.	LOPSTR	2004	DBLP DOI BibTeX RDF
27	J. B. Wells, Boris Yakobowski	Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis.	LOPSTR	2004	DBLP DOI BibTeX RDF
27	Claudio Sacerdoti Coen	Mathematical Libraries as Proof Assistant Environments.	MKM	2004	DBLP DOI BibTeX RDF
27	Jean-Marc Andreoli, Laurent Mazaré	Concurrent Construction of Proof-Nets.	CSL	2003	DBLP DOI BibTeX RDF
27	David Delahaye	Free-Style Theorem Proving.	TPHOLs	2002	DBLP DOI BibTeX RDF
27	Jesse Alt, Sergei N. Artëmov	Reflective lambda-Calculus.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
27	Ralph Matthes	Interpolation for Natural Deduction with Generalized Eliminations.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF
27	Olivier Danvy	Many Happy Returns.	TLCA	2001	DBLP DOI BibTeX RDF
27	Shin-ya Katsumata, Atsushi Ohori	Proof-Directed De-compilation of Low-Level Code.	ESOP	2001	DBLP DOI BibTeX RDF
27	Ralph Matthes	Monotone Inductive and Coinductive Constructors of Rank 2.	CSL	2001	DBLP DOI BibTeX RDF
27	Pierre-Louis Curien	Abstract Machines, Control, and Sequents.	APPSEM	2000	DBLP DOI BibTeX RDF