Showing 1–21 of 21 results for author: David, R

POSTER: spaceQUIC: Securing Communication in Computationally Constrained Spacecraft

Authors: Joshua Smailes, Razvan David, Sebastian Kohler, Simon Birnbach, Ivan Martinovic

Abstract: Recent years have seen a rapid increase in the number of CubeSats and other small satellites in orbit - these have highly constrained computational and communication resources, but still require robust secure communication to operate effectively. The QUIC transport layer protocol is designed to provide efficient communication with cryptography guarantees built-in, with a particular focus on netw… ▽ More Recent years have seen a rapid increase in the number of CubeSats and other small satellites in orbit - these have highly constrained computational and communication resources, but still require robust secure communication to operate effectively. The QUIC transport layer protocol is designed to provide efficient communication with cryptography guarantees built-in, with a particular focus on networks with high latency and packet loss. In this work we provide spaceQUIC, a proof of concept implementation of QUIC for NASA's "core Flight System" satellite operating system, and assess its performance. △ Less

Submitted 22 May, 2023; originally announced May 2023.

Comments: 2 pages, 2 figures; the first two authors contributed equally to this paper

E2E Segmentation in a Two-Pass Cascaded Encoder ASR Model

Authors: W. Ronny Huang, Shuo-Yiin Chang, Tara N. Sainath, Yanzhang He, David Rybach, Robert David, Rohit Prabhavalkar, Cyril Allauzen, Cal Peyser, Trevor D. Strohman

Abstract: We explore unifying a neural segmenter with two-pass cascaded encoder ASR into a single model. A key challenge is allowing the segmenter (which runs in real-time, synchronously with the decoder) to finalize the 2nd pass (which runs 900 ms behind real-time) without introducing user-perceived latency or deletion errors during inference. We propose a design where the neural segmenter is integrated wi… ▽ More We explore unifying a neural segmenter with two-pass cascaded encoder ASR into a single model. A key challenge is allowing the segmenter (which runs in real-time, synchronously with the decoder) to finalize the 2nd pass (which runs 900 ms behind real-time) without introducing user-perceived latency or deletion errors during inference. We propose a design where the neural segmenter is integrated with the causal 1st pass decoder to emit a end-of-segment (EOS) signal in real-time. The EOS signal is then used to finalize the non-causal 2nd pass. We experiment with different ways to finalize the 2nd pass, and find that a novel dummy frame injection strategy allows for simultaneous high quality 2nd pass results and low finalization latency. On a real-world long-form captioning task (YouTube), we achieve 2.4% relative WER and 140 ms EOS latency gains over a baseline VAD-based segmenter with the same cascaded encoder. △ Less

Submitted 5 March, 2023; v1 submitted 28 November, 2022; originally announced November 2022.

Comments: ICASSP 2023

EOSC-LIFE WP4 TOOLBOX: Toolbox for sharing of sensitive data -- a concept description

Authors: Jan-Willem Boiten, Christian Ohmann, Ayodeji Adeniran, Steve Canham, Monica Cano Abadia, Gauthier Chassang, Maria Luisa Chiusano, Romain David, Maddalena Fratelli, Phil Gribbon, Petr Holub, Rebecca Ludwig, Michaela Th. Mayrhofer, Mihaela Matei, Arshiya Merchant, Maria Panagiotopoulou, Luca Pireddu, Alex Sanchez Pla, Irene Schlünder, George Tsamis, Harald Wagener

Abstract: The Horizon 2020 project EOSC-Life brings together the 13 Life Science 'ESFRI' research infrastructures to create an open, digital and collaborative space for biological and medical research. Sharing sensitive data is a specific challenge within EOSC-Life. For that reason, a toolbox is being developed, providing information to researchers who wish to share and/or use sensitive data in a cloud envi… ▽ More The Horizon 2020 project EOSC-Life brings together the 13 Life Science 'ESFRI' research infrastructures to create an open, digital and collaborative space for biological and medical research. Sharing sensitive data is a specific challenge within EOSC-Life. For that reason, a toolbox is being developed, providing information to researchers who wish to share and/or use sensitive data in a cloud environment in general, and the European Open Science Cloud in particular. The sensitivity of the data may arise from its personal nature but can also be caused by intellectual property considerations, biohazard concerns, or the Nagoya protocol. The toolbox will not create new content, instead, it will allow researchers to find existing resources that are relevant for sharing sensitive data across all participating research infrastructures (F in FAIR). The toolbox will provide links to recommendations, procedures, and best practices, as well as to software (tools) to support data sharing and reuse. It will be based upon a tagging (categorisation) system, allowing consistent labelling and categorisation of resources. The current design document provides an outline for the anticipated toolbox, as well as its basic principles regarding content and sustainability. △ Less

Submitted 28 July, 2022; originally announced July 2022.

A Unified Cascaded Encoder ASR Model for Dynamic Model Sizes

Authors: Shao** Ding, Weiran Wang, Ding Zhao, Tara N. Sainath, Yanzhang He, Robert David, Rami Botros, Xin Wang, Rina Panigrahy, Qiao Liang, Dongseong Hwang, Ian McGraw, Rohit Prabhavalkar, Trevor Strohman

Abstract: In this paper, we propose a dynamic cascaded encoder Automatic Speech Recognition (ASR) model, which unifies models for different deployment scenarios. Moreover, the model can significantly reduce model size and power consumption without loss of quality. Namely, with the dynamic cascaded encoder model, we explore three techniques to maximally boost the performance of each model size: 1) Use separa… ▽ More In this paper, we propose a dynamic cascaded encoder Automatic Speech Recognition (ASR) model, which unifies models for different deployment scenarios. Moreover, the model can significantly reduce model size and power consumption without loss of quality. Namely, with the dynamic cascaded encoder model, we explore three techniques to maximally boost the performance of each model size: 1) Use separate decoders for each sub-model while sharing the encoders; 2) Use funnel-pooling to improve the encoder efficiency; 3) Balance the size of causal and non-causal encoders to improve quality and fit deployment constraints. Overall, the proposed large-medium model has 30% smaller size and reduces power consumption by 33%, compared to the baseline cascaded encoder model. The triple-size model that unifies the large, medium, and small models achieves 37% total size reduction with minimal quality loss, while substantially reducing the engineering efforts of having separate models. △ Less

Submitted 24 June, 2022; v1 submitted 13 April, 2022; originally announced April 2022.

Comments: Accepted by INTERSPEECH 2022

Tied & Reduced RNN-T Decoder

Authors: Rami Botros, Tara N. Sainath, Robert David, Emmanuel Guzman, Wei Li, Yanzhang He

Abstract: Previous works on the Recurrent Neural Network-Transducer (RNN-T) models have shown that, under some conditions, it is possible to simplify its prediction network with little or no loss in recognition accuracy (arXiv:2003.07705 [eess.AS], [2], arXiv:2012.06749 [cs.CL]). This is done by limiting the context size of previous labels and/or using a simpler architecture for its layers instead of LSTMs.… ▽ More Previous works on the Recurrent Neural Network-Transducer (RNN-T) models have shown that, under some conditions, it is possible to simplify its prediction network with little or no loss in recognition accuracy (arXiv:2003.07705 [eess.AS], [2], arXiv:2012.06749 [cs.CL]). This is done by limiting the context size of previous labels and/or using a simpler architecture for its layers instead of LSTMs. The benefits of such changes include reduction in model size, faster inference and power savings, which are all useful for on-device applications. In this work, we study ways to make the RNN-T decoder (prediction network + joint network) smaller and faster without degradation in recognition performance. Our prediction network performs a simple weighted averaging of the input embeddings, and shares its embedding matrix weights with the joint network's output layer (a.k.a. weight tying, commonly used in language modeling arXiv:1611.01462 [cs.LG]). This simple design, when used in conjunction with additional Edit-based Minimum Bayes Risk (EMBR) training, reduces the RNN-T Decoder from 23M parameters to just 2M, without affecting word-error rate (WER). △ Less

Submitted 15 September, 2021; originally announced September 2021.

Journal ref: Proc. Interspeech 2021, 4563-4567

Kubernetes Autoscaling: YoYo Attack Vulnerability and Mitigation

Authors: Ronen Ben David, Anat Bremler Barr

Abstract: In recent years, we have witnessed a new kind of DDoS attack, the burst attack(Chai, 2013; Dahan, 2018), where the attacker launches periodic bursts of traffic overload on online targets. Recent work presents a new kind of Burst attack, the YoYo attack (Bremler-Barr et al., 2017) that operates against the auto-scaling mechanism of VMs in the cloud. The periodic bursts of traffic loads cause the au… ▽ More In recent years, we have witnessed a new kind of DDoS attack, the burst attack(Chai, 2013; Dahan, 2018), where the attacker launches periodic bursts of traffic overload on online targets. Recent work presents a new kind of Burst attack, the YoYo attack (Bremler-Barr et al., 2017) that operates against the auto-scaling mechanism of VMs in the cloud. The periodic bursts of traffic loads cause the auto-scaling mechanism to oscillate between scale-up and scale-down phases. The auto-scaling mechanism translates the flat DDoS attacks into Economic Denial of Sustainability attacks (EDoS), where the victim suffers from economic damage accrued by paying for extra resources required to process the traffic generated by the attacker. However, it was shown that YoYo attack also causes significant performance degradation since it takes time to scale-up VMs. In this research, we analyze the resilience of Kubernetes auto-scaling against YoYo attacks. As containerized cloud applications using Kubernetes gain popularity and replace VM-based architecture in recent years. We present experimental results on Google Cloud Platform, showing that even though the scale-up time of containers is much lower than VM, Kubernetes is still vulnerable to the YoYo attack since VMs are still involved. Finally, we evaluate ML models that can accurately detect YoYo attack on a Kubernetes cluster. △ Less

Submitted 8 May, 2021; v1 submitted 2 May, 2021; originally announced May 2021.

Comments: Paper contains 14 pages, 4 figures. This paper was presented in CLOSER 2021 conference on April 28,2021. CLOSER 2021 is the 11th International Conference on Cloud Computing and Services Science, which was organized by INSTICC. The paper is available soon at SCITEPRESS Digital Library

Journal ref: Volume 1: CLOSER 2021,ISBN 978-989-758-510-4, pages 34-44

39 Hints to Facilitate the Use of Semantics for Data on Agriculture and Nutrition

Authors: Caterina Caracciolo, Sophie Aubin, Clement Jonquet, Emna Amdouni, Romain David, Leyla Garcia, Brandon Whitehead, Catherine Roussey, Armando Stellato, Ferdinando Villa

Abstract: In this paper, we report on the outputs and adoption of the Agrisemantics Working Group of the Research Data Alliance (RDA), consisting of a set of recommendations to facilitate the adoption of semantic technologies and methods for the purpose of data interoperability in the field of agriculture and nutrition. From 2016 to 2019, the group gathered researchers and practitioners at the crossing poin… ▽ More In this paper, we report on the outputs and adoption of the Agrisemantics Working Group of the Research Data Alliance (RDA), consisting of a set of recommendations to facilitate the adoption of semantic technologies and methods for the purpose of data interoperability in the field of agriculture and nutrition. From 2016 to 2019, the group gathered researchers and practitioners at the crossing point between information technology and agricultural science, to study all aspects in the life cycle of semantic resources: conceptualization, edition, sharing, standardization, services, alignment, long term support. First, the working group realized a landscape study, a study of the uses of semantics in agrifood, then collected use cases for the exploitation of semantics resources-a generic term to encompass vocabularies, terminologies, thesauri, ontologies. The resulting requirements were synthesized into 39 "hints" for users and developers of semantic resources, and providers of semantic resource services. We believe adopting these recommendations will engage agrifood sciences in a necessary transition to leverage data production, sharing and reuse and the adoption of the FAIR data principles. The paper includes examples of adoption of those requirements, and a discussion of their contribution to the field of data science. △ Less

Submitted 15 December, 2020; originally announced December 2020.

Journal ref: CODATA Data Science Journal, Committee on Data for Science and Technology (CODATA), 2020, 19 (1)

TensorFlow Lite Micro: Embedded Machine Learning on TinyML Systems

Authors: Robert David, Jared Duke, Advait Jain, Vijay Janapa Reddi, Nat Jeffries, Jian Li, Nick Kreeger, Ian Nappier, Meghna Natraj, Shlomi Regev, Rocky Rhodes, Tiezhen Wang, Pete Warden

Abstract: Deep learning inference on embedded devices is a burgeoning field with myriad applications because tiny embedded devices are omnipresent. But we must overcome major challenges before we can benefit from this opportunity. Embedded processors are severely resource constrained. Their nearest mobile counterparts exhibit at least a 100 -- 1,000x difference in compute capability, memory availability, an… ▽ More Deep learning inference on embedded devices is a burgeoning field with myriad applications because tiny embedded devices are omnipresent. But we must overcome major challenges before we can benefit from this opportunity. Embedded processors are severely resource constrained. Their nearest mobile counterparts exhibit at least a 100 -- 1,000x difference in compute capability, memory availability, and power consumption. As a result, the machine-learning (ML) models and associated ML inference framework must not only execute efficiently but also operate in a few kilobytes of memory. Also, the embedded devices' ecosystem is heavily fragmented. To maximize efficiency, system vendors often omit many features that commonly appear in mainstream systems, including dynamic memory allocation and virtual memory, that allow for cross-platform interoperability. The hardware comes in many flavors (e.g., instruction-set architecture and FPU support, or lack thereof). We introduce TensorFlow Lite Micro (TF Micro), an open-source ML inference framework for running deep-learning models on embedded systems. TF Micro tackles the efficiency requirements imposed by embedded-system resource constraints and the fragmentation challenges that make cross-platform interoperability nearly impossible. The framework adopts a unique interpreter-based approach that provides flexibility while overcoming these challenges. This paper explains the design decisions behind TF Micro and describes its implementation details. Also, we present an evaluation to demonstrate its low resource requirement and minimal run-time performance overhead. △ Less

Submitted 13 March, 2021; v1 submitted 16 October, 2020; originally announced October 2020.

On hybrid precoder/combiner for downlink mmWave massive MU-MIMO systems

Authors: Alvaro Javier Ortega, Raimundo Sampaio-Neto, Rodrigo Pereira David

Abstract: We propose four hybrid combiner/precoder for downlink mmWave massive MU-MIMO systems. The design of a hybrid combiner/precoder is divided in two parts, analog and digital. The system baseband model shows that the signal processed by the mobile station can be interpreted as a received signal in the presence of colored Gaussian noise, therefore, since the digital part of the combiner and precoder do… ▽ More We propose four hybrid combiner/precoder for downlink mmWave massive MU-MIMO systems. The design of a hybrid combiner/precoder is divided in two parts, analog and digital. The system baseband model shows that the signal processed by the mobile station can be interpreted as a received signal in the presence of colored Gaussian noise, therefore, since the digital part of the combiner and precoder do not have constraints for their generation, their designs can be based on any traditional signal processing that takes into account this kind of noise. To the best of our knowledge, this was not considered by previous works. A more realistic and appropriate design is described in this paper. Also, the approaches adopted in the literature for the designing of the combiner'/precoder' analog parts do not try to avoid or even reduce the inter user/symbol interference, they concentrate on increasing the signal-to-noise ratio (SNR). We propose a simple solution that decreases the interference while maintaining large SNR. In addition, one of the proposed hybrid combiners reaches the maximum value of our objective function according with the Hadamard's inequality. Numerical results illustrate the BER performance improvements resulting from our proposals. In addition, a simple detection approach can be used for data estimation without significant performance loss. △ Less

Submitted 31 October, 2019; originally announced November 2019.

Comments: 28 pages, 11 figures

Balanced Facilities on Random Graphs

Authors: Roee David, Nimrod Talmon

Abstract: Given a graph G with n vertices and k players, each of which is placing a facility on one of the vertices of G, we define the score of the i'th player to be the number of vertices for which, among all players, the facility placed by the i'th player is the closest. A placement is balanced if all players get roughly the same score. A graph is balanced if all placements on it are balanced. Viewing ba… ▽ More Given a graph G with n vertices and k players, each of which is placing a facility on one of the vertices of G, we define the score of the i'th player to be the number of vertices for which, among all players, the facility placed by the i'th player is the closest. A placement is balanced if all players get roughly the same score. A graph is balanced if all placements on it are balanced. Viewing balancedness as a desired property in various scenarios, in this paper we study balancedness properties of graphs, concentrating on random graphs and on expanders. We show that, while both random graphs and expanders tend to have good balancedness properties, random graphs are, in general, more balanced. In addition, we formulate and prove intractability of the combinatorial problem of deciding whether a given graph is balanced; then, building upon our analysis on random graphs and expanders, we devise two efficient algorithms which, with high probability, generate balancedness certificates. Our first algorithm is based on graph traversal, while the other relies on spectral properties. △ Less

Submitted 5 June, 2017; originally announced June 2017.

Targeting Infeasibility Questions on Obfuscated Codes

Authors: Robin David, Sébastien Bardin, Jean-Yves Marion

Abstract: Software deobfuscation is a crucial activity in security analysis and especially, in malware analysis. While standard static and dynamic approaches suffer from well-known shortcomings, Dynamic Symbolic Execution (DSE) has recently been proposed has an interesting alternative, more robust than static analysis and more complete than dynamic analysis. Yet, DSE addresses certain kinds of questions enc… ▽ More Software deobfuscation is a crucial activity in security analysis and especially, in malware analysis. While standard static and dynamic approaches suffer from well-known shortcomings, Dynamic Symbolic Execution (DSE) has recently been proposed has an interesting alternative, more robust than static analysis and more complete than dynamic analysis. Yet, DSE addresses certain kinds of questions encountered by a reverser namely feasibility questions. Many issues arising during reverse, e.g. detecting protection schemes such as opaque predicates fall into the category of infeasibility questions. In this article, we present the Backward-Bounded DSE, a generic, precise, efficient and robust method for solving infeasibility questions. We demonstrate the benefit of the method for opaque predicates and call stack tampering, and give some insight for its usage for some other protection schemes. Especially, the technique has successfully been used on state-of-the-art packers as well as on the government-grade X-Tunnel malware -- allowing its entire deobfuscation. Backward-Bounded DSE does not supersede existing DSE approaches, but rather complements them by addressing infeasibility questions in a scalable and precise manner. Following this line, we propose sparse disassembly, a combination of Backward-Bounded DSE and static disassembly able to enlarge dynamic disassembly in a guaranteed way, hence getting the best of dynamic and static disassembly. This work paves the way for robust, efficient and precise disassembly tools for heavily-obfuscated binaries. △ Less

Submitted 16 December, 2016; originally announced December 2016.

ACM Class: D.4.6; K.6.5; D.2.4

On the Complexity of Closest Pair via Polar-Pair of Point-Sets

Authors: Roee David, Karthik C. S., Bundit Laekhanukit

Abstract: Every graph $G$ can be represented by a collection of equi-radii spheres in a $d$-dimensional metric $Δ$ such that there is an edge $uv$ in $G$ if and only if the spheres corresponding to $u$ and $v$ intersect. The smallest integer $d$ such that $G$ can be represented by a collection of spheres (all of the same radius) in $Δ$ is called the sphericity of $G$, and if the collection of spheres are no… ▽ More Every graph $G$ can be represented by a collection of equi-radii spheres in a $d$-dimensional metric $Δ$ such that there is an edge $uv$ in $G$ if and only if the spheres corresponding to $u$ and $v$ intersect. The smallest integer $d$ such that $G$ can be represented by a collection of spheres (all of the same radius) in $Δ$ is called the sphericity of $G$, and if the collection of spheres are non-overlap**, then the value $d$ is called the contact-dimension of $G$. In this paper, we study the sphericity and contact dimension of the complete bipartite graph $K_{n,n}$ in various $L^p$-metrics and consequently connect the complexity of the monochromatic closest pair and bichromatic closest pair problems. △ Less

Submitted 15 November, 2018; v1 submitted 10 August, 2016; originally announced August 2016.

Comments: The paper was previously titled, "The Curse of Medium Dimension for Geometric Problems in Almost Every Norm"

ACM Class: F.2.2

Random walks with the minimum degree local rule have $O(n^2)$ cover time

Authors: Roee David, Uriel Feige

Abstract: For a simple (unbiased) random walk on a connected graph with $n$ vertices, the cover time (the expected number of steps it takes to visit all vertices) is at most $O(n^3)$. We consider locally biased random walks, in which the probability of traversing an edge depends on the degrees of its endpoints. We confirm a conjecture of Abdullah, Cooper and Draief [2015] that the min-degree local bias rule… ▽ More For a simple (unbiased) random walk on a connected graph with $n$ vertices, the cover time (the expected number of steps it takes to visit all vertices) is at most $O(n^3)$. We consider locally biased random walks, in which the probability of traversing an edge depends on the degrees of its endpoints. We confirm a conjecture of Abdullah, Cooper and Draief [2015] that the min-degree local bias rule ensures a cover time of $O(n^2)$. For this we formulate and prove the following lemma about spanning trees. Let $R(e)$ denote for edge $e$ the minimum degree among its two endpoints. We say that a weight function $W$ for the edges is feasible if it is nonnegative, dominated by $R$ (for every edge $W(e) \le R(e)$) and the sum over all edges of the ratios $W(e)/R(e)$ equals $n-1$. For example, in trees $W(e) = R(e)$, and in regular graphs the sum of edge weights is $d(n-1)$. {\bf Lemma:} for every feasible $W$, the minimum weight spanning tree has total weight $O(n)$. For regular graphs, a similar lemma was proved by Kahn, Linial, Nisan and Saks [1989]. △ Less

Submitted 18 July, 2016; v1 submitted 28 April, 2016; originally announced April 2016.

Comments: 19 pages. 4 figures

On the effect of randomness on planted 3-coloring models

Authors: Roee David, Uriel Feige

Abstract: We present the hosted coloring framework for studying algorithmic and hardness results for the $k$-coloring problem. There is a class ${\cal H}$ of host graphs. One selects a graph $H\in{\cal H}$ and plants in it a balanced $k$-coloring (by partitioning the vertex set into $k$ roughly equal parts, and removing all edges within each part). The resulting graph $G$ is given as input to a polynomial t… ▽ More We present the hosted coloring framework for studying algorithmic and hardness results for the $k$-coloring problem. There is a class ${\cal H}$ of host graphs. One selects a graph $H\in{\cal H}$ and plants in it a balanced $k$-coloring (by partitioning the vertex set into $k$ roughly equal parts, and removing all edges within each part). The resulting graph $G$ is given as input to a polynomial time algorithm that needs to $k$-color $G$ (any legal $k$-coloring would do -- the algorithm is not required to recover the planted $k$-coloring). Earlier planted models correspond to the case that ${\cal H}$ is the class of all $n$-vertex $d$-regular graphs, a member $H\in{\cal H}$ is chosen at random, and then a balanced $k$-coloring is planted at random. Blum and Spencer [1995] designed algorithms for this model when $d=n^δ$ (for $0<δ\le1$), and Alon and Kahale [1997] managed to do so even when $d$ is a sufficiently large constant. The new aspect in our framework is that it need not involve randomness. In one model within the framework (with $k=3$) $H$ is a $d$ regular spectral expander (meaning that except for the largest eigenvalue of its adjacency matrix, every other eigenvalue has absolute value much smaller than $d$) chosen by an adversary, and the planted 3-coloring is random. We show that the 3-coloring algorithm of Alon and Kahale [1997] can be modified to apply to this case. In another model $H$ is a random $d$-regular graph but the planted balanced $3$-coloring is chosen by an adversary, after seeing $H$. We show that for a certain range of average degrees somewhat below $\sqrt{n}$, finding a 3-coloring is NP-hard. Together these results (and other results that we have) help clarify which aspects of randomness in the planted coloring model are the key to successful 3-coloring algorithms. △ Less

Submitted 16 March, 2016; originally announced March 2016.

Comments: 56 pages, one figure. To be appear in STOC 2016

MSC Class: 68Q01

About the range property for H

Authors: René David, Karim Nour

Abstract: Recently, A. Polonsky has shown that the range property fails for H. We give here some conditions on a closed term that imply that its range has an infinite cardinality. Recently, A. Polonsky has shown that the range property fails for H. We give here some conditions on a closed term that imply that its range has an infinite cardinality. △ Less

Submitted 21 January, 2014; v1 submitted 2 November, 2013; originally announced November 2013.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 1 (January 21, 2014) lmcs:849

A short proof that adding some permutation rules to $β$ preserves $SN$

Authors: Rene David

Abstract: I show that, if a term is $SN$ for $β$, it remains $SN$ when some permutation rules are added. I show that, if a term is $SN$ for $β$, it remains $SN$ when some permutation rules are added. △ Less

Submitted 5 November, 2010; originally announced November 2010.

Comments: Theoretical Computer Science, 2010

Strong normalization results by translation

Authors: René David, Karim Nour

Abstract: We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system. We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system. △ Less

Submitted 18 May, 2009; originally announced May 2009.

Comments: Submitted to APAL

Counting proofs in propositional logic

Authors: René David, Marek Zaionc

Abstract: We give a procedure for counting the number of different proofs of a formula in various sorts of propositional logic. This number is either an integer (that may be 0 if the formula is not provable) or infinite. We give a procedure for counting the number of different proofs of a formula in various sorts of propositional logic. This number is either an integer (that may be 0 if the formula is not provable) or infinite. △ Less

Submitted 18 May, 2009; originally announced May 2009.

Journal ref: Archive for Mathematical Logic 48 (2009) P 185-199

A direct proof of the confluence of combinatory strong reduction

Authors: René David

Abstract: I give a proof of the confluence of combinatory strong reduction that does not use the one of lambda-calculus. I also give simple and direct proofs of a standardization theorem for this reduction and the strong normalization of simply typed terms. I give a proof of the confluence of combinatory strong reduction that does not use the one of lambda-calculus. I also give simple and direct proofs of a standardization theorem for this reduction and the strong normalization of simply typed terms. △ Less

Submitted 15 May, 2009; originally announced May 2009.

Comments: To appear in TCS

A short proof that adding some permutation rules to beta preserves SN

Authors: René David

Abstract: I show that, if a term is $SN$ for $β$, it remains $SN$ when some permutation rules are added. I show that, if a term is $SN$ for $β$, it remains $SN$ when some permutation rules are added. △ Less

Submitted 27 April, 2009; v1 submitted 20 April, 2009; originally announced April 2009.

Asymptotically almost all λ-terms are strongly normalizing

Authors: René David, Katarzyna Grygiel, Jakub Kozic, Christophe Raffalli, Guillaume Theyssier, Marek Zaionc

Abstract: We present quantitative analysis of various (syntactic and behavioral) properties of random λ-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term. Surprisingly, in combinatory logic (the translation of the λ-calculus into combinators), the result is exactly opposite. We show that almost all term… ▽ More We present quantitative analysis of various (syntactic and behavioral) properties of random λ-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random term. Surprisingly, in combinatory logic (the translation of the λ-calculus into combinators), the result is exactly opposite. We show that almost all terms are not strongly normalizing. This is due to the fact that any fixed combinator almost always appears in a random combinator. △ Less

Submitted 13 February, 2013; v1 submitted 31 March, 2009; originally announced March 2009.

ACM Class: G.2.1

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 1 (February 15, 2013) lmcs:848